We introduce and study hierarchies of extensions of the propositional modal and temporal languages with pairs of new syntactic devices: point of reference-reference pointer which enable semantic references to be made within a formula. We propose three different but equivalent semantics for the extended languages, discuss and compare their expressiveness. The languages with reference pointers are shown to have great expressive power (especially when their frugal syntax is taken into account), perspicuous semantics, and simple deductive systems. For instance, (...) Kamp's and Stavi's temporal operators, as well as nominals (names, clock variables), are definable in them. Universal validity in these languages is proved undecidable. The basic modal and temporal logics with reference pointers are uniformly axiomatized and a strong completeness theorem is proved for them and extended to some classes of their extensions. (shrink)

In the 4th century BC, the Greek philosopher Diodoros Chronos gave a temporal definition of necessity. Because it connects modality and temporality, this definition is of interest to philosophers working within branching time or branching space-time models. This definition of necessity can be formalized and treated within a logical framework. We give a survey of the several known modal and temporal logics of abstract space-time structures based on the real numbers and the integers, considering three different accessibility (...) relations between spatio-temporal points. (shrink)

In this paper we suggest adding to predicate modal and temporal logic a locality predicate W which gives names to worlds (or time points). We also study an equal time predicate D(x, y)which states that two time points are at the same distance from the root. We provide the systems studied with complete axiomatizations and illustrate the expressive power gained for modal logic by simulating other logics. The completeness proofs rely on the fairly intuitive notion (...) of a configuration in order to use a proof technique similar to a Henkin completion mixed with a tableau construction. The main elements of the completeness proofs are given for each case, while purely technical results are grouped in the appendix. (shrink)

We generalize an observation made by Goldblatt in "Diodorean modality in Minkowski spacetime" by proving that each -dimensional integral spacetime frame equipped with Robb's irreflexive `after' relation determines a unique temporal logic. Our main result is that, unlike -dimensional spacetime where, as Goldblatt has shown, the Diodorean modal logic is the same for each frame , in the case of -dimensional integral spacetime, the frame determines a unique Diodorean modal logic.

The paper presents a survey of author's results on definable fixed points in modal, temporal, and intuitionistic propositional logics. The well-known Fixed Point Theorem considers the modalized case, but here we investigate the positive case. We give a classification of fixed point theorems, describe some classes of models with definable least fixed points of positive operators, special positive operators, and give some examples of undefinable least fixed points. Some other interesting phenomena are discovered – definability by formulas that (...) do not preserve positivity of parameters and definability by finite sets of formulas. We also consider negative operators, graded modalities, construct undefinable inflationary fixed points, and put some problems. (shrink)

Developed by Arthur Prior, Temporal Logic allows to represent temporal information on a logical system using modal operators such as P, F, H or G, whose intuitive meaning is “it was sometime in the Past...”, “it will be sometime in the Future...”, “it Has always been in the past...” and “it will always Going to be in the future...” respectively. Valuation of formulae built from these operators are carried out on Kripke semantics, so Modal (...) class='Hi'>Logic and Temporal Logic are consequently related. In fact, Temporal Logic is an extension of Modal one. Even when both logics mechanisms are able to formalize modal-temporal information with some accuracy, they suffer from a lack of expressiveness which Hybrid Logic can solve. Indeed, one of the problems of Modal Logic consists in its incapacity of naming specific points inside a model. As Temporal Logic is based on it, it cannot make such a thing neither. But First-Order Logic does can by means of constants and equality relation. Hybrid Logic, which results from combining Modal Logic and First-Order Logic, may solve this shortcoming. The main aim of this paper is to explain how Hybrid Logic emanates from Modal and Temporal ones in order to show what it adds to both logics with regard to information representation, why it is more expressive than them and what relation it maintains with the First-Order Correspondence Language. (shrink)

Developed by Arthur Prior, Temporal Logic allows to represent temporal information on a logical system using modal operators such as P, F, H or G, whose intuitive meaning is “it was sometime in the Past...”, “it will be sometime in the Future...”, “it Has always been in the past...” and “it will always Going to be in the future...” respectively. Valuation of formulae built from these operators are carried out on Kripke semantics, so Modal (...) class='Hi'>Logic and Temporal Logic are consequently related. In fact, Temporal Logic is an extension of Modal one. Even when both logics mechanisms are able to formalize modal-temporal information with some accuracy, they suffer from a lack of expressiveness which Hybrid Logic can solve. Indeed, one of the problems of Modal Logic consists in its incapacity of naming specific points inside a model. As Temporal Logic is based on it, it cannot make such a thing neither. But First-Order Logic does can by means of constants and equality relation. Hybrid Logic, which results from combining Modal Logic and First-Order Logic, may solve this shortcoming. The main aim of this paper is to explain how Hybrid Logic emanates from Modal and Temporal ones in order to show what it adds to both logics with regard to information representation, why it is more expressive than them and what relation it maintains with the First-Order Correspondence Language. (shrink)

In this paper we improve the results of [2] by proving the product f.m.p. for the product of minimal n-modal and minimal n-temporal logic. For this case we modify the finite depth method introduced in [1]. The main result is applied to identify new fragments of classical first-order logic and of the equational theory of relation algebras, that are decidable and have the finite model property.

The traditional Dung networks depict arguments as atomic and study the relationships of attack between them. This can be generalised in two ways. One is to consider various forms of attack, support, feedback, etc. Another is to add content to nodes and put there not just atomic arguments but more structure, e.g. proofs in some logic or simply just formulas from a richer language. This paper offers to use temporal and modal language formulas to represent arguments in (...) the nodes of a network. The suitable semantics for such networks is Kripke semantics. We also introduce a new key concept of usability of an argument. This is the beginning of a continuing research for adding contents to the nodes of an argumentation network. This research will allow us to address notions like ?what does it exactly mean for a node to attack another? or ?what does it mean for a network to be consistent? or ?can we give proper proof rules to manipulate networks?, and more. (shrink)

Hybridization is a method invented by Arthur Prior for extending the expressive power of modal languages. Although developed in interesting ways by Robert Bull, and by the Sofia school , the method remains little known. In our view this has deprived temporal logic of a valuable tool.The aim of the paper is to explain why hybridization is useful in temporal logic. We make two major points, the first technical, the second conceptual. First, we show that (...) hybridization gives rise to well-behaved logics that exhibit an interesting synergy between modal and classical ideas. This synergy, obvious for hybrid languages with full first-order expressive strength, is demonstrated for a weaker local language capable of defining the Until operator; we provide a minimal axiomatization, and show that in a wide range of temporally interesting cases extended completeness results can be obtained automatically. Second, we argue that the idea of sorted atomic symbols which underpins the hybrid enterprise can be developed further. To illustrate this, we discuss the advantages and disadvantages of a simple hybrid language which can quantify over paths. (shrink)

This chapter contains sections titled: Modal Concepts The Semantics of Modalities and Systems of Modal Logic Modality and Quantification Deontic, Epistemic, and Temporal Modalities Epistemic Logic Deontic Logic Temporal Frames Conditional Obligations and Rules of Detachment.

The present study on al-Dīn Suhrawardī's Ḥikmat al-Ishrāq, develops some preliminary explorations on his logic under the background of his remarkable epistemology of pis some witness of d resence. The paper paves the way for responding to the challenges of Tony Street on the compatibility of Suhrawardī's critique of Ibn Sīnā with the development of a temporal and modal syllogism that at first sight seems quite close to that of Ibn Sīnā. In fact, Suhrawardī's modalities are to (...) be understood as the different ways a predicate relates to its subject rather than as propositional operators. Accordingly, necessarily necessary modality relates actual instances (presences) of the Subject-Term with actual (presences) of the Predicate-Term; in contrast, necessarily contingent modality relates these terms conditionally, notably involving states of the Subject-Term within time intervals. Suhrawardī's main innovation, so we claim, is the explicit dialectical role presences or actual instances have in his modal-temporal logic, and particularly so in shaping his notion of contingency that admits both a generic and an individual or de re form of plenitude. (shrink)

This paper introduces a framework for direct surface composition by online update. The surface string is interpreted as is, with each morpheme in turn updating the input state of information and attention. A formal representation language, Logic of Centering, is defined and some crosslinguistic constraints on lexical meanings and compositional operations are formulated.

Prior's approach to time has been neglected by semanticists for several reasons. The main one, we believe, is the inability of Priorean tense logic to refer to times. The second one, is the inability to account for some important features of natural language such as temporal anaphora and the role of temporal constructions in discourse. Priorean tense logic has, however, one important advantage over other accounts: the internal perspective of time (due to its modal nature). (...) This paper examines extensions of Priorean tense logic in which reference to times is possible, focusing on the so-called hybrid temporal logic. We will outline some of its main features and analyze some of its philosophical implications. (shrink)

Prior's three-valued modal logic Q was developed as a philosophically interesting modal logic. Thus, we should be able to modify Q as a temporal logic. Although a temporal version of Q was suggested by Prior, the subject has not been fully explored in the literature. In this paper, we develop a three-valued temporal logic $Q_t $ and give its axiomatization and semantics. We also argue that $Q_t $ provides a smooth solution (...) to the problem of future contingents. (shrink)

We define bisimulations for temporal logic with Since and Until. This new notion is compared to existing notions of bisimulations, and then used to develop the basic model theory of temporal logic with Since and Until. Our results concern both invariance and definability. We conclude with a brief discussion of the wider applicability of our ideas.

The essay introduces a non-Diodorean, non-Kantian temporal modal semantics based on part-whole, rather than class, theory. Formalizing Edmund Husserl’s theory of inner time consciousness, §3 uses his protention and retention concepts to define a relation of self-awareness on intentional events. §4 introduces a syntax and two-valued semantics for modal first-order predicate object-languages, defines semantic assignments for variables and predicates, and truth for formulae in terms of the axiomatic version of Edmund Husserl’s dependence ontology (viz. the Calculus [CU] (...) of Urelements) introduced by The Ontology of Intentionality I & II. It then uses the §3 results to define the modalities of truth, and §5 extends the semantics to identity claims. §6 defines and contrasts synthetic a priori truths to analytic a priori truths, and §7 compares Brentano School noetic semantic and Leibnizian possible-world semantic perspectives on modality. The essay argues that the modal logics it defines semantically are two-valued, first-order versions of the type of language which Husserl viewed as the language of any ontology of experience (i.e. of any science), and conceived as the logic of intentionality. (shrink)

This work concerns the use of operators for past and future contingency in Priorean temporal logic. We will develop a system named C_t, whose language includes a propositional constant and prove that (I) C_t is complete with respect to a certain class of general frames and (II) the usual operators for past and future necessity are definable in such system. Furthermore, we will introduce the extension C_t(lin) that can be interpreted on linear and transitive general frames. The theoretical (...) result of the current work is that contingency can be treated as a primitive notion in reasoning about temporal modalities. (shrink)

In this paper, we study temporal logic for finite linear structures and surjective bounded morphisms between them. We give a characterisation of such structures by modal formulas and show that every pair of linear structures with a bounded morphism between them can be uniquely characterised by a temporal formula up to an isomorphism. As the main result, we prove Kripke completeness of the logic with respect to the class of finite linear structures with bounded morphisms (...) between them. (shrink)

This paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible paths. We (...) then consider a hierarchy of natural classes of trees and bundled trees arising from a given class of linear orders and show that in general they provide different semantics. We also discuss transfer of definability from linear orders to trees and introduce a uniform translation from Priorean to Peircean formulae which transfers definability of properties of linear orders to definability of properties of all paths in trees. (shrink)

Temporal justification logic is a new family of temporal logics of knowledge in which the knowledge of agents is modelled using a justification logic. In this paper, we present various temporal justification logics involving both past and future time modalities. We combine Artemov’s logic of proofs with linear temporal logic with past, and we also investigate several principles describing the interaction of justification and time. We present two kinds of semantics for our (...) temporal justification logics, one based on interpreted systems and Fitting models and the other based on Mkrtychev models, and further, we establish soundness and completeness. We show that the internalization property holds in some of the temporal justification logics. We further investigate the two well-known epistemic-temporal notions of no forgetting and no learning in the framework of justification logics. Finally, we present temporal justification logics that avoid the logical omniscience problem. (shrink)

We present a variant of ATL with incomplete information which includes the distributed knowledge operators corresponding to synchronous action and perfect recall. The cooperation modalities assume the use the distributed knowledge of coalitions and accordingly refer to perfect recall incomplete information strategies. We propose a model-checking algorithm for the logic. It is based on techniques for games with imperfect information and partially observable objectives, and involves deciding emptiness for automata on infinite trees. We also propose an axiomatic system and (...) prove its completeness for a rather expressive subset. As for the constructs left outside this completely axiomatised subset, we present axioms by which they can be defined in the subset on the class of models in which every state has finitely many successors and give a complete axiomatisation for a “flat” subset of the logic with these constructs included. (shrink)

In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted over partial orders (\nsbcdt\ (...) for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented. (shrink)

The papers collected in this volume exemplify some of the trends in current approaches to logic, language and computation. Written by authors with varied academic backgrounds, the contributions are intended for an interdisciplinary audience. The first part of this volume addresses issues relevant for multi-agent systems: reasoning with incomplete information, reasoning about knowledge and beliefs, and reasoning about games. Proofs as formal objects form the subject of Part II. Topics covered include: contributions on logical frameworks, linear logic, and (...) different approaches to formalized reasoning. Part III focuses on representations and formal methods in linguistic theory, addressing the areas of comparative and temporal expressions, modal subordination, and compositionality. (shrink)

A succession of events is a sequence of events such that after one event is finished, the next one occurs successively. In this paper, we extended linear temporal logic with a new modality to capture the case that a sequence of events successively occurs. We compared the expressivity between this extended linear temporal logic and the standard linear temporal logic.

Alternating-time temporal logic (ATL) is a branching time temporal logic in which statements about what coalitions of agents can achieve by strategic cooperation can be expressed. Alternating-time temporal epistemic logic (ATEL) extends ATL by adding knowledge modalities, with the usual possible worlds interpretation. This paper investigates how properties of agents’ actions can be expressed in ATL in general, and how properties of the interaction between action and knowledge can be expressed in ATEL in particular. (...) One commonly discussed property is that an agent should know about all available actions, i.e., that the same actions should be available in indiscernible states. Van der Hoek and Wooldridge suggest a syntactic expression of this semantic property. This paper shows that this correspondence in fact does not hold. Furthermore, it is shown that the semantic property is not expressible in ATEL at all. In order to be able to express common and interesting properties of action in general and of the interaction between action and knowledge in particular, a generalization of the coalition modalities of ATL is proposed. The resulting logics, ATL-A and ATEL-A, have increased expressiveness without loosing ATL’s and ATEL’s tractability of model checking. (shrink)

We combine linear temporal logic (with both past and future modalities) with a deontic version of justification logic to provide a framework for reasoning about time and epistemic and normative reasons. In addition to temporal modalities, the resulting logic contains two kinds of justification assertions: epistemic justification assertions and deontic justification assertions. The former presents justification for the agent’s knowledge and the latter gives reasons for why a proposition is obligatory. We present two kinds of (...) semantics for the logic: one based on Fitting models and the other based on neighborhood models. The use of neighborhood semantics enables us to define the dual of deontic justification assertions properly, which corresponds to a notion of permission in deontic logic. We then establish the soundness and completeness of an axiom system of the logic with respect to these semantics. Further, we formalize the Protagoras versus Euathlus paradox in this logic and present a precise analysis of the paradox, and also briefly discuss Leibniz’s solution. (shrink)

This paper proposes a semantic description of the linear step-like temporal multi-agent logic with the universal modality \(\mathcal{LTK}.sl_U\) based on the idea of non-reflexive non-transitive nature of time. We proved a finite model property and projective unification for this logic.

Future Logic is an original, and wide-ranging treatise of formal logic. It deals with deduction and induction, of categorical and conditional propositions, involving the natural, temporal, extensional, and logical modalities. Traditional and Modern logic have covered in detail only formal deduction from actual categoricals, or from logical conditionals (conjunctives, hypotheticals, and disjunctives). Deduction from modal categoricals has also been considered, though very vaguely and roughly; whereas deduction from natural, temporal and extensional forms of conditioning (...) has been all but totally ignored. As for induction, apart from the elucidation of adductive processes (the scientific method), almost no formal work has been done. This is the first work ever to strictly formalize the inductive processes of generalization and particularization, through the novel methods of factorial analysis, factor selection and formula revision. This is the first work ever to develop a formal logic of the natural, temporal and extensional types of conditioning (as distinct from logical conditioning), including their production from modal categorical premises. Future Logic contains a great many other new discoveries, organized into a unified, consistent and empirical system, with precise definitions of the various categories and types of modality (including logical modality), and full awareness of the epistemological and ontological issues involved. Though strictly formal, it uses ordinary language, wherever symbols can be avoided. Among its other contributions: a full list of the valid modal syllogisms (which is more restrictive than previous lists); the main formalities of the logic of change (which introduces a dynamic instead of merely static approach to classification); the first formal definitions of the modal types of causality; a new theory of class logic, free of the Russell Paradox; as well as a critical review of modern metalogic. But it is impossible to list briefly all the innovations in logical science — and therefore, epistemology and ontology — this book presents; it has to be read for its scope to be appreciated. (shrink)

After the seminal work of Kraus, Lehmann and Magidor (formally known as the KLM approach) on conditionals and preferential models, many aspects of defeasibility in more complex formalisms have been studied in recent years. Examples of these aspects are the notion of typicality in description logic and defeasible necessity in modal logic. We discuss a new aspect of defeasibility that can be expressed in the case of temporal logic, which is the normality in an execution. (...) In this contribution, we take Linear Temporal Logic (LTL) as case study for this defeasible aspect. LTL has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. However, some systems may presents exceptions at some innocuous time points where they can be tolerated, or conversely, exceptions at other crucial time points where they need to be addressed. In order to ensure the reliability of such systems, we study a preferential extension of LTL, called defeasible linear temporal logic (LTL ~ ). In the first part of this paper, we show how semantics of KLM's preferential models can be integrated with LTL. We also discuss the addition of non-monotonic temporal operators as a way to formalise defeasible properties of these systems. The second part of this paper is a study of the satisfiability problem of LTL ~ sentences. Based on Sistla and Clarke's work on the complexity of the classical LTL language, we show the bounded-model property of two fragments of LTL ~ language. Moreover, we provide a procedure to check the satisfiability of sentences in both of these fragments. (shrink)

ABSTRACT In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar; it is a temporal logic that contains connectives for representing the beliefs of agents. In (...) addition to a complete formal definition of the two logics and their decision procedures, the paper includes a brief review of their applications in AI and mainstream computer science, correctness proofs for the decision procedures, a number of worked examples illustrating the decision procedures, and some pointers to further work. (shrink)

ABSTRACT We critically review two extant paradigms for understanding the systematic interaction between modality and tense, as well as their respective modifications designed to do justice to the contingency of time’s structure and composition. We show that on either type of theory, as well as their respective modifications, some principles prove logically valid whose truth might sensibly be questioned on metaphysical grounds. These considerations lead us to devise a more general logical framework that allows accommodation of those metaphysical views that (...) its predecessors rule out by fiat. (shrink)

The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules (...) in special reduced normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(NBox+-wC) and show how to reduce the problem for admissibility to the decidability of TL(NBox+-wC) itself using definable universal modalities. (shrink)

This paper generalises and complements the work on combining temporal logics started by Finger and Gabbay [11, 10]. We present proofs of transference of soundness, completeness and decidability for the temporalisation of logics T for any flow of time, eliminating the original restriction that required linear time for the transference of those properties through logic combination. We also generalise such results to the external application of a multi-modal system containing any number of connectives with arbitrary arity, that (...) respect normality.This generalisation over generic flows of time propagates to other combinations of logics that can be interpreted in terms of temporalisations. In this way, the independent combination of temporal logics is studied over generic flows of time. We show the transfer of soundness, completeness and decidability for independent combination of temporal logics. Finally, we also discuss the independent combination of any finite number of normal multi-modal logics. (shrink)

The most popular method of incorporating time into a formal logic is based on the work of Arthur Prior. It treats tenses as operators on sentences. In this essay I show a serious problem with that approach, a confusion of scheme versus proposition, which makes any system built in that way incoherent. I will compare how other formal logics deal with the scheme versus proposition distinction and find that only for formal modal logics does the same problem arise. (...) I then compare Prior’s approach to other ways of taking time into account in formal logics. (shrink)

For branching-time temporal logic based on an Ockhamist semantics, we explore a temporal language extended with two additional syntactic tools. For reference to the set of all possible futures at a moment of time we use syntactically designated restricted variables called fan-names. For reference to all possible futures alternative to the actual one we use a modification of a difference modality, localized to the set of all possible futures at the actual moment of time.We construct an axiomatic (...) system for this extended branching-time logic and prove its soundness and completeness with respect to bundle tree semantics. Finally, we show how our axiomatic system can be extended with a variety of important additional operators, such as Since and Until, a global difference operator, operators for undivided and divided histories, reference pointers, etc. (shrink)

Although formal system verification has been around for many years, little attention was given to the case where the specification of the system has to be changed. This may occur due to a failure in capturing the clients’ requirements or due to some change in the domain (think for example of banking systems that have to adapt to different taxes being imposed). We are interested in having methods not only to verify properties, but also to suggest how the system model (...) should be changed so that a property would be satisfied. For this purpose, we will use techniques from the area of Belief Revision, that deals with the problem of changing a knowledge base in view of new information. In the last thirty years, several authors have contributed with change operations and ways of characterizing them. However, most of the work concentrates on knowledge bases represented using classical propositional logic. In the last decade, there have been efforts to apply belief revision theory to description and modal logics. In this work, we analyze what is needed for a theory of belief revision which can be applied to the temporal logic, such as the Computation Tree Logic (CTL). In particular, we illustrate different alternatives for formalizing the concept of revision of CTL. Our interest in this particular logic comes both from practical issues, since it is used for software specification, as from theoretical issues, as it is a non-compact logic and most existing results rely on compactness. We focus here on the revision of CTL models and present a characterization result for the revision of partial models. (shrink)

In their simplest form, hybrid languages are propositional modal languages which can refer to states. They were introduced by Arthur Prior, the inventor of tense logic, and played an important role in his work: because they make reference to specific times possible, they remove the most serious obstacle to developing modal approaches to temporal representation and reasoning. However very little is known about the computational complexity of hybrid temporal logics.In this paper we analyze the complexity (...) of the satisfiability problem of a number of hybrid temporal logics: the basic hybrid language over transitive trees; nominal Until logic; and referential interval logic. We discuss the effects of including nominals, the @ operator, the somewhere modality E, and the difference operator D. Adding nominals to tense logic leads for several frame-classes to an increase in complexity of the satisfiability problem from PSPACE to EXPTIME. On transitive trees, however, the satisfiability problem for this language can be decided in PSPACE. Along the way we make a detour through hybrid propositional dynamic logic: we establish upper bounds for a number of temporal logics by generalizing results due to Passy and Tinchev [29] and De Giacomo [16]. We conclude with some remarks on the relevance of our results to description logic, and draw attention to the utility of the spypoint technique for proving upper and lower bounds. (shrink)

ABSTRACT Many temporal and modal logic languages can be regarded as subsets of first order logic, i.e. the semantics of a temporal logic formula is given as a first order condition on points of the underlying models (Kripke structures). Often the set of possible models is restricted to models which are trees. A temporal logic language is (first order) expressively complete, if for every first order condition for a node of a tree (...) there exists an equivalent temporal formula which expresses the same condition. In this paper expressive completeness of the temporal logic language with the set of operators U (until), S (since), and X k (k-next) is proved, and the result is extended to various other tree-like structures. (shrink)