A Survey on Temporal Logics
---
paper_title: Formal methods for the specification and design of real-time safety critical systems

paper_content:

Abstract Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies that fail to meet stringent timing constraints have resulted in catastrophic failures. This article surveys formal methods for specifying, designing, and verifying real-time systems so as to improve their safety and reliability.
---
paper_title: Duration Calculus: A Formal Approach to Real-Time Systems

paper_content:

The Duration Calculus (DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses real numbers to model time, and Boolean-valued (i.e. 0, 1-valued) functions over time to model states of real-time systems. The duration of a state in a time interval is the accumulated presence time of the state in the interval. DC extends interval logic with a calculus to specify and reason about properties of state durations. The first paper of DC was published in 1991, and dozens of papers of DC have been published since then, which cover developments of logical calculi, their applications and mechanical support tools. This paper will give a brief introduction to DC and also an overview of the research of DC.
---
paper_title: Word Meaning and Montague Grammar

paper_content:

A four position racking mechanism for a circuit breaker in a cubicle or housing providing Connected, Test, Disconnect and Out positions. The racking lead screw is mounted in the circuit breaker structure in its own support. The rear end of the racking screw is threaded to engage and move a travelling nut which rides in guide slots. The outer ends of the travelling nut engage a pair of connecting links which rotate a pivoted roller bracket. The roller bracket carries a racking roller which engages a cam slot in a member extending from the rear portion of the cubicle or housing. The shape of the cam slot plus the increasing lever arm of the connecting links around the pivot pin on the nut provide a variable racking force which is needed for primary disconnect contact engagement. The central positioning of the racking mechanism makes it suitable for any width of circuit breaker. The racking mechanism is interlocked with the closing mechanism; releasable locking means and interlock means are provided to limit the operation of the racking mechanism to conditions which are safe for the operator; thus, the unlocking of the racking mechanism after the breaker is tripped will hold the trip mechanism and hold it trip free as long as the racking mechanism is unlocked. An indexing element for the slide for the locking mechanism is provided for all the positions of the circuit breaker.
---
paper_title: Allen linear (interval) temporal logic - : Translation to LTL and monitor synthesis

paper_content:

The relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen's interval algebra (or Allen's temporal logic, abbreviated ATL) and linear temporal logic (LTL). A discrete variant of ATL is defined, called Allen linear temporal logic (ALTL), whose models are ω-sequences of timepoints. It is shown that any ALTL formula can be linearly translated into an equivalent LTL formula, thus enabling the use of LTL techniques on ALTL requirements. This translation also implies the NP-completeness of ATL satisfiability. Then the problem of monitoring ALTL requirements is investigated, showing that it reduces to checking satisfiability; the similar problem for unrestricted LTL is known to require exponential space. An effective monitoring algorithm for ALTL is given, which has been implemented and experimented with in the context of planning applications.
---
paper_title: Real-time interval logic for reasoning about executions of real-time programs

paper_content:

Research on the testing and debugging of distributed real-time programs now focuses on more formal approaches to specification and testing. Temporal logic is a natural candidate for this since it can specify properties of event and state sequences. However, the absence of any concept of real-time limits the application of temporal logic to non real-time behavior. This paper presents an extension of the interval logic of Schwartz et al. [SMSVP83], by increasing the expressive power of the logic (with respect to real time) while retaining its intuitive appeal and understandability. The extensions are added in a “layer” that can be stripped away if formal verification is the goal, or retained if timing behavior must be tested. The extensions include: the ability to deal with real time (as in [JM86b, JM86a, OW87, NA88]); more powerful interval specification mechanisms; a limited form of quantification; and the direct expression of event predicates (as in [LeD86]). Since our work is intended to yield practical tools for software testers, we emphasize the ease of expressing the complex timing properties of real-time software (e.g. periodic behavior, performance constraints), and we demonstrate the use of the interval logic on some real-time examples that represent a test of the expressiveness and understandability of the notation.
---
paper_title: Events, Instants and Temporal Reference

paper_content:

The truth of my claim: ‘It is raining’ depends on the time at which I made it. It was true if and only if it was indeed raining (in my vicinity) at that time. Similarly my assertion ‘it has been raining’, made at time t, is true if there was a time t′ preceding t such that it rained at t′.
---
paper_title: Temporal and Modal Logic

paper_content:

Publisher Summary This chapter discusses temporal and modal logic. The chapter describes a multiaxis classification of systems of temporal logic. The chapter describes the framework of linear temporal logic. In both its propositional and first-order forms, linear temporal logic has been widely employed in the specification and verification of programs. The chapter describes the competing framework of branching temporal logic, which has seen wide use. It also explains how temporal logic structures can be used to model concurrent programs using non-determinism and fairness. The chapter also discusses other modal and temporal logics in computer science. The chapter describes the formal syntax and semantics of Propositional Linear Temporal Logic (PLTL). The chapter also describes the formal syntax and semantics for two representative systems of propositional branching-time temporal logics.
---
paper_title: A decidability result for a second order process logic

paper_content:

We prove the decidability of the validity problem for a rather general language for talking about computations. As corollaries of our result, we obtain some decidability results of Pratt, Constable, Fischer-Ladner, and Pnueli and also a new decidability result for deterministic propositional dynamic logic.
---
paper_title: Temporal logics for real-time system specification

paper_content:

The specification of reactive and real-time systems must be supported by formal, mathematically-founded methods in order to be satisfactory and reliable. Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formulas, including temporal constraints, events, and the relationships between the two. In the last ten years, temporal logics have reached a high degree of expressiveness. Most of the temporal logics proposed in the last few years can be used for specifying reactive systems, although not all are suitable for specifying real-time systems. In this paper we present a series of criteria for assessing the capabilities of temporal logics for the specification, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness, the logic's order, presence of a metric for time, the type of temporal operators, the fundamental time entity, and the structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer, a set of typical specifications is identified and used with most of the temporal logics considered, thus presenting the reader with a number of real examples.
---
paper_title: Maintaining knowledge about temporal intervals

paper_content:

An interval-based temporal logic is introduced, together with a computationally effective reasoning algorithm based on constraint propagation. This system is notable in offering a delicate balance between
---
paper_title: Intervals and tenses

paper_content:

Neither question (1) nor question (2) posed on page 446 have been adequately answered in this paper. Regarding (1) we have merely given functor maps onto the object languages of physical theories and regarding (2) we have merely described the algebraic structure of observables. A more satisfactory treatment will most likely involve (1) a generalization to algebraic categories, universal algebra and model theory in such a way as to capture the full inference structure of (perhaps van Fraassen's modal) quantum logic, and (2) the introduction of the category of differentiable manifolds in order to capture the full symplectic structure of (perhaps Chernoff-Marsden's) Hamiltonian dynamics. (See van Fraassen [4] and Chernoff-Marsden [5] in Other References.)
---
paper_title: Extending Interval Logic to Real Time Systems

paper_content:

Interval logic is a temporal logic that provides a higher-level framework for specifying distributed systems. The concepts of intervals and interval composition form the basic structure of many specifications. Interval logic allows such conceptual requirements to be stated rather directly and intuitively.
---
paper_title: Duration Calculus: A Formal Approach to Real-Time Systems

paper_content:

The Duration Calculus (DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses real numbers to model time, and Boolean-valued (i.e. 0, 1-valued) functions over time to model states of real-time systems. The duration of a state in a time interval is the accumulated presence time of the state in the interval. DC extends interval logic with a calculus to specify and reason about properties of state durations. The first paper of DC was published in 1991, and dozens of papers of DC have been published since then, which cover developments of logical calculi, their applications and mechanical support tools. This paper will give a brief introduction to DC and also an overview of the research of DC.
---
paper_title: Process logic: Expressiveness, decidability, completeness

paper_content:

Abstract A process logic (PL) is defined that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). A deductive system for PL is given which includes the Segerberg axioms for PDL and it is proved that it is complete. It is also shown that PL is decidable.
---
paper_title: Reasoning About Digital Circuits

paper_content:

Abstract : Predicate logic is a powerful and general descriptive formalism with a long history of development. However, since the logic's underlying semantics have no notion of time, statements such as I increases by 2 and The bit signal X rises from 0 to 1 can not be directly expressed. The author presents a formalism called interval temporal logic (ITL) that augments standard predicate logic with time-dependent operators. ITL is like discrete linear-time temporal logic but includes time intervals. The behavior of programs and hardware devices can often be decomposed into successively smaller intervals of activity. State transitions can be characterized by properties relating the initial and final values of variables over intervals. Furthermore, these time periods provide a convenient framework for introducing quantitative timing details. After giving some motivation for reasoning about hardware, he presents the propositional and first-order syntax and semantics of ITL. Demonstrated is ITL's utility for uniformly describing the structure and dynamics of a wide variety of timing-dependent digital circuits. Devices discussed include delay elements, adders, latches, flip-flops, counters, random-access memories, a clocked multiplication circuit and the Am2901 bit slice. ITL also provides a means for expressing properties of such specifications. Also examine are such concepts as device equivalence and internal states. Propositional ITL is shown to be undecidable although useful subsets are of relatively reasonable computational complexity. (Author)
---
paper_title: Temporal logic : mathematical foundations and computational aspects

paper_content:

1. The handling of time: introduction and survey 2. Semantical presentation of temporal connectives 3. Axiomatic presentation of propositional temporal connectives 4. Predicate temporal logics 5. Temporal logics presented in the predicate calculus: language-metalanguage 6. A general theory of axiomatization for propositional temporal logic 7. Basic many-dimensional systems 8. Propositional quantifiers and fixed point operators 9. Expressive power of one-dimensional temporal connectives: basic concepts 10. Expressive completeness of Since and Until over integer and real time 11. Expressive completeness of Stavi connectives over general linear time 12. Further expressive completeness results 13. H-dimension 14. Adding a temporal dimension to a logic system 15. Decidability in temporal logic Bibliography Notation Index Index of Systems Index
---
paper_title: Decidability of Interval Temporal Logics over Split-Frames via Granularity

paper_content:

Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of artificial intelligence and computer science. Unfortunately, most interval temporal logics proposed in the literature have been shown to be (highly) undecidable. Decidable fragments of these logics have been obtained by imposing severe restrictions on their expressive power.In this paper, we propose a new interval temporal logic, called Split Logic, which is equipped with operators borrowed from other interval temporal logics, but is interpreted over specific interval structures based on a layered view of the temporal domain. We show that there exists a straightforward correspondence between Split Logic and the first-order fragments of the monadic theories of time granularity proposed in the literature. This connection allows us to transfer existing decidability results for such theories to Split Logic.
---
paper_title: Parts: A Study in Ontology

paper_content:

The relationship of part to whole is one of the most fundamental there is, yet until now there has been no full-length study of this concept. This book shows that mereology, the formal theory of part and whole, is essential to ontology. Peter Simons surveys and criticizes previous theories, especially the standard extensional view, and proposes a more adequate account which encompasses both temporal and modal considerations in detail. This has far-reaching consequences for our understanding of such classical philosophical concepts as identity, individual, class, substance and accident, matter, form, essence, dependence, and integral whole. It also enables the author to offer new solutions to longstanding problems surrounding these concepts, such as the Ship of Theseus Problem and the issue of mereological essentialism. The author shows by his use of formal techniques that classical philosophical problems are amenable to rigorous treatment, and the book represents a synthesis of issues and methods from the analytical tradition and from the older continental realist tradition of Brentano and the early Husserl. The book is aimed at philosophers, logicians, and linguists.
---
paper_title: A Critical Examination of Allen's Theory of Action and Time

paper_content:

Abstract J.F. Allen's theory of time and action is examined and found to be unsuitable for representing facts about continuous change. A series of revisions to Allen's theory is proposed in order to accommodate this possibility. The principal revision is a diversification of the temporal ontology to include instants on the same footing as intervals; a distinction is also made between two kinds of property, called states of position and states of motion, with respect to the logic of their temporal incidence. As a consequence of these revisions, it is also found necessary to diversify the range of predicates specifying temporal location. Finally, it is argued that Allen's category of processes is superfluous, since it can be assimilated with the category of properties. The implications of this assimilation for the representation of sentences containing verbs in the progressive aspect are discussed.
---
paper_title: The Glory of the Past

paper_content:

An extension of propositional temporal logic that includes operators referring to a bounded past is considered. An exponential time decision procedure and a complete axiomatic system are presented. A suggested normal form leads to a syntactic classification of safety and liveness formulae. The adequacy of temporal logic to modular verification is examined. Finally we present the notion of α-fairness which is proved to fully capture the behavior of probabilistic finite state programs.
---
paper_title: Quantitative Temporal Logics over the Reals : PSpace and below

paper_content:

In many cases, the addition of metric operators to qualitative temporal logics (TLs) increases the complexity of satisfiability by at least one exponential: while common qualitative TLs are complete for NP or PSPACE, their metric extensions are often ExpSpACE-complete or even undecidable. In this paper, we exhibit several metric extensions of qualitative TLs of the real line that are at most PSPACE-complete, and analyze the transition from NP to PSPACE for such logics. Our first result is that the logic obtained by extending since-until logic of the real line with the operators 'sometime within n time units in the past/future' is still PSpACE-complete. In contrast to existing results, we also capture the case where n is coded in binary and the finite variability assumption is not made. To establish containment in PSPACE, we use a novel reduction technique that can also be used to prove tight upper complexity bounds for many other metric TLs in which the numerical parameters to metric operators are coded in binary. We then consider metric TLs of the reals that do not offer any qualitative temporal operators. In such languages, the complexity turns out to depend on whether binary or unary coding of parameters is assumed: satisfiability is still PSPACE-complete under binary coding, but only NP-complete under unary coding.
---
paper_title: Counting LTL

paper_content:

This paper presents a quantitative extension for the linear-time temporal logic LTL allowing to specify the number of states satisfying certain sub-formulas along paths. We give decision procedures for the satisfiability and model checking of this new temporal logic and study the complexity of the corresponding problems. Furthermore we show that the problems become undecidable when more expressive constraints are considered.
---
paper_title: The temporal logic of programs

paper_content:

A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.
---
paper_title: Verification of Concurrent Programs: Temporal Proof Principles

paper_content:

In this paper, the second of a series on the application of temporal logic to concurrent programs, we present proof methods for establishing invariance (safety) and eventuality (liveness) properties.
---
paper_title: On the temporal analysis of fairness

paper_content:

The use of the temporal logic formalism for program reasoning is reviewed. Several aspects of responsiveness and fairness are analyzed, leading to the need for an additional temporal operator: the 'until' operator -U. Some general questions involving the 'until' operator are then discussed. It is shown that with the addition of this operator the temporal language becomes expressively complete. Then, two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.
---
paper_title: The complexity of propositional linear temporal logics

paper_content:

We consider the complexity of satisfiability and determination of truth in a particular finite structure for different propositional linear temporal logics. We show that both the above problems are NP-complete for the logic with F operator and are PSPACE-complete for the logics with F,X, with U, with U,S,X, and Wolper's extended logic with regular operators [Wo81].
---
paper_title: A Resolution Method for Temporal Logic

paper_content:

In this paper, a resolution method for propositional temporal logic is presented. Temporal formulae, incorporating both past-time and future-time temporal operators, are converted to Separated Normal Form (SNF), then both non-temporal and temporal resolution rules are applied. The resolution method is based on classical resolution, but incorporates a temporal resolution rule that can be implemented efficiently using a graph-theoretic approach.
---
paper_title: The Power of Temporal Proofs

paper_content:

Abstract Some methods for reasoning about concurrent programs and hardware devices have been based on proof systems for temporal logic. Unfortunately, all effective proof systems for temporal logic are incomplete for the standard semantics, in the sense that some formulas hold in every intended model but cannot be proved. We evaluate and compare the power of several proof systems for temporal logic. Specifically, we relate temporal systems to classical systems with explicit time parameters. A typical temporal system turns out to be incomplete in a strong sense; we exhibit a short, valid formula it fails to prove. We suggest the addition of new rules to define auxiliary predicates. With these rules, we obtain nonstandard soundness and completeness results. In particular, one of the simple temporal systems we describe is as powerful as Peano Arithmetic.
---
paper_title: Reasoning About Knowledge

paper_content:

Reasoning about knowledge—particularly the knowledge of agents who reason about the world and each other's knowledge—was once the exclusive province of philosophers and puzzle solvers. More recently, this type of reasoning has been shown to play a key role in a surprising number of contexts, from understanding conversations to the analysis of distributed computer algorithms. Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed systems, artificial intelligence, and game theory. It brings eight years of work by the authors into a cohesive framework for understanding and analyzing reasoning about knowledge that is intuitive, mathematically well founded, useful in practice, and widely applicable. The book is almost completely self-contained and should be accessible to readers in a variety of disciplines, including computer science, artificial intelligence, linguistics, philosophy, cognitive science, and game theory. Each chapter includes exercises and bibliographic notes.
---
paper_title: Decidability and incompleteness results for first-order temporal logics of linear time

paper_content:

ABSTRACT The question of axiomatizability of first-order temporal logics is studied w.r.t. different semantics and several restrictions on the language. The validity problem for logics admitting flexible interpretations of the predicate symbols or allowing at least binary predicate symbols is shown to be Π1 1-complete. In contrast, it is decidable for temporal logics with rigid monadic predicate symbols but without function symbols and identity.
---
paper_title: Axiomatizing the Monodic Fragment of First-Order Temporal Logic

paper_content:

Abstract It is known that even seemingly small fragments of the first-order temporal logic over the natural numbers are not recursively enumerable. In this paper we show that the monodic (not monadic, where this result does not hold) fragment is an exception by constructing its finite Hilbert-style axiomatization. We also show that the monodic fragment with equality is not recursively axiomatizable.
---
paper_title: On the Completeness and Decidability of a Restricted First Order Linear Temporal Logic

paper_content:

The paper describes a class of FC-sequents of a restricted first order linear temporal logic with “next” and “always”. It is shown that the first order linear temporal logic is finitary complete for FC-sequents. If FC-sequents are logically decidable, i.e., all sequents, constructed from all possible subformulas of logical formulas of FC-sequents are decidable in first-order logic, then FC-sequents are decidable in the restricted first order linear temporal logic. To obtain these results a saturation calculus [6, 7] for FC-sequents is constructed.
---
paper_title: Decidable fragments of first-order temporal logics

paper_content:

Abstract In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps.
---
paper_title: Axiomatising first-order temporal logic: Until and since over linear time

paper_content:

We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.We also add a few axioms to find a sound and complete axiomatisation for the first order temporal logic of Until and Since over rational numbers time.
---
paper_title: Efficient checking of temporal integrity constraints using bounded history encoding

paper_content:

We present an efficient implementation method for temporal integrity constraints formulated in Past Temporal Logic. Although the constraints can refer to past states of the database, their checking does not require that the entire database history be stored. Instead, every database state is extended with auxiliary relations that contain the historical information necessary for checking constraints. Auxiliary relations can be implemented as materialized relational views.
---
paper_title: On the Restraining Power of Guards

paper_content:

Guarded fragments of first-order logic were recently introduced by Andreka, van Benthem and Nemeti; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment ( GF ) and the loosely guarded fragment ( LGF ) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is E xptime -complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable.
---
paper_title: Temporal logic : mathematical foundations and computational aspects

paper_content:

1. The handling of time: introduction and survey 2. Semantical presentation of temporal connectives 3. Axiomatic presentation of propositional temporal connectives 4. Predicate temporal logics 5. Temporal logics presented in the predicate calculus: language-metalanguage 6. A general theory of axiomatization for propositional temporal logic 7. Basic many-dimensional systems 8. Propositional quantifiers and fixed point operators 9. Expressive power of one-dimensional temporal connectives: basic concepts 10. Expressive completeness of Since and Until over integer and real time 11. Expressive completeness of Stavi connectives over general linear time 12. Further expressive completeness results 13. H-dimension 14. Adding a temporal dimension to a logic system 15. Decidability in temporal logic Bibliography Notation Index Index of Systems Index
---
paper_title: Temporal Logic in Information Systems

paper_content:

Temporal logic is obtained by adding temporal connectives to a logic language. Explicit references to time are hidden inside the temporal connectives. Different variants of temporal logic use different sets of such connectives. In this chapter, we survey the fundamental varieties of temporal logic and describe their applications in information systems.
---
paper_title: Decidable fragments of first-order temporal logics

paper_content:

Abstract In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps.
---
paper_title: The Classical Decision Problem

paper_content:

1. Introduction: The Classical Decision Problem.- 1.1 The Original Problem.- 1.2 The Transformation of the Classical Decision Problem.- 1.3 What Is and What Isn't in this Book.- I. Undecidable Classes.- 2. Reductions.- 2.1 Undecidability and Conservative Reduction.- 2.1.1 The Church-Turing Theorem and Reduction Classes.- 2.1.2 Trakhtenbrot's Theorem and Conservative Reductions.- 2.1.3 Inseparability and Model Complexity.- 2.2 Logic and Complexity.- 2.2.1 Propositional Satisfiability.- 2.2.2 The Spectrum Problem and Fagin's Theorem.- 2.2.3 Capturing Complexity Classes.- 2.2.4 A Decidable Prefix-Vocabulary Class.- 2.3 The Classifiability Problem.- 2.3.1 The Problem.- 2.3.2 Well Partially Ordered Sets.- 2.3.3 The Well Quasi Ordering of Prefix Sets.- 2.3.4 The Well Quasi Ordering of Arity Sequences.- 2.3.5 The Classifiability of Prefix-Vocabulary Sets.- 2.4 Historical Remarks.- 3. Undecidable Standard Classes for Pure Predicate Logic.- 3.1 The Kahr Class.- 3.1.1 Domino Problems.- 3.1.2 Formalization of Domino Problems by $$[\forall \exists \forall , (0,\omega )]$$-Formulae.- 3.1.3 Graph Interpretation of $$[\forall \exists \forall , (0,\omega )]$$-Formulae.- 3.1.4 The Remaining Cases Without $$\exists *$$.- 3.2 Existential Interpretation for $$[{{\forall }^{3}}\exists *, (0,1)]$$.- 3.3 The Gurevich Class.- 3.3.1 The Proof Strategy.- 3.3.2 Reduction to Diagonal-Freeness.- 3.3.3 Reduction to Shift-Reduced Form.- 3.3.4 Reduction toFi-Elimination Form.- 3.3.5 Elimination of MonadicFi.- 3.3.6 The Kostyrko-Genenz and Suranyi Classes.- 3.4 Historical Remarks.- 4. Undecidable Standard Classes with Functions or Equality.- 4.1 Classes with Functions and Equality.- 4.2 Classes with Functions but Without Equality.- 4.3 Classes with Equality but Without Functions: the Goldfarb Classes 161 4.3.1 Formalization of Natural Numbers in $$[{{\forall }^{3}}\exists *, (\omega ,\omega ),(0)]$$=.- 4.3.2 Using Only One Existential Quantifiers.- 4.3.3 Encoding the Non-Auxiliary Binary Predicates.- 4.3.4 Encoding the Auxiliary Binary Predicates of NUM*.- 4.4 Historical Remarks.- 5. Other Undecidable Cases.- 5.1 Krom and Horn Formulae.- 5.1.1 Krom Prefix Classes Without Functions or Equality.- 5.1.2 Krom Prefix Classes with Functions or Equality.- 5.2 Few Atomic Subformulae.- 5.2.1 Few Function and Equality Free Atoms.- 5.2.2 Few Equalities and Inequalities.- 5.2.3 Horn Clause Programs With One Krom Rule.- 5.3 Undecidable Logics with Two Variables.- 5.3.1 First-Order Logic with the Choice Operator.- 5.3.2 Two-Variable Logic with Cardinality Comparison.- 5.4 Conjunctions of Prefix-Vocabulary Classes.- 5.4.1 Reduction to the Case of Conjunctions.- 5.4.2 Another Classifiability Theorem.- 5.4.3 Some Results and Open Problems.- 5.5 Historical Remarks.- II. Decidable Classes and Their Complexity.- 6. Standard Classes with the Finite Model Property.- 6.1 Techniques for Proving Complexity Results.- 6.1.1 Domino Problems Revisited.- 6.1.2 Succinct Descriptions of Inputs.- 6.2 The Classical Solvable Cases.- 6.2.1 Monadic Formulae.- 6.2.2 The Bernays-Schonfinkel-Ramsey Class.- 6.2.3 The Godel-Kalmar-Schutte Class: a Probabilistic Proof.- 6.3 Formulae with One ?.- 6.3.1 A Satisfiability Test for [?*??*, all, all].- 6.3.2 The Ackermann Class.- 6.3.3 The Ackermann Class with Equality.- 6.4 Standard Classes of Modest Complexity.- 6.4.1 The Relational Classes in P, NP and Co-NP.- 6.4.2 Fragments of the Theory of One Unary Function.- 6.4.3 Other Functional Classes.- 6.5 Finite Model Property vs. Infinity Axioms.- 6.6 Historical Remarks.- 7. Monadic Theories and Decidable Standard Classes with Infinity Axioms.- 7.1 Automata, Games and Decidability of Monadic Theories.- 7.1.1 Monadic Theories.- 7.1.2 Automata on Infinite Words and the Monadic Theory of One Successor.- 7.1.3 Tree Automata, Rabin's Theorem and Forgetful De terminacy.- 7.1.4 The Forgetful Determinacy Theorem for Graph Games.- 7.2 The Monadic Second-Order Theory of One Unary Function.- 7.2.1 Decidability Results for One Unary Function.- 7.2.2 The Theory of One Unary Function is not Elementary Recursive.- 7.3 The Shelah Class.- 7.3.1 Algebras with One Unary Operation.- 7.3.2 Canonic Sentences.- 7.3.3 Terminology and Notation.- 7.3.4 1-Satisfiability.- 7.3.5 2-Satisfiability.- 7.3.6 Refinements.- 7.3.7 Villages.- 7.3.8 Contraction.- 7.3.9 Towns.- 7.3.10 The Final Reduction.- 7.4 Historical Remarks.- 8. Other Decidable Cases.- 8.1 First-Order Logic with Two Variables.- 8.2 Unification and Applications to the Decision Problem.- 8.2.1 Unification.- 8.2.2 Herbrand Formulae.- 8.2.3 Positive First-Order Logic.- 8.3 Decidable Classes of Krom Formulae.- 8.3.1 The Chain Criterion.- 8.3.2 The Aanderaa-Lewis Class.- 8.3.3 The Maslov Class.- 8.4 Historical Remarks.- A. Appendix: Tiling Problems.- A.1 Introduction.- A.2 The Origin Constrained Domino Problem.- A.3 Robinson's Aperiodic Tile Set.- A.4 The Unconstrained Domino Problem.- A.5 The Periodic Problem and the Inseparability Result.- Annotated Bibliography.
---
paper_title: A tableau decision algorithm for modalized ALC with constant domains

paper_content:

The aim of this paper is to construct a tableau decision algorithm for the modal description logic K ALC with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an ALC-formula ϕ with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether ϕ is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be 'practical' even for logics of rather high complexity. This gives us grounds to believe that, although the satisfiability problem for K ALC is known to be NEXPTIME-complete, by providing a tableau decision algorithm we demonstrate that highly expressive description logics with modal operators have a chance to be implementable. The paper gives a solution to an open problem of Baader and Laux [5].
---
paper_title: Axiomatizing the Monodic Fragment of First-Order Temporal Logic

paper_content:

Abstract It is known that even seemingly small fragments of the first-order temporal logic over the natural numbers are not recursively enumerable. In this paper we show that the monodic (not monadic, where this result does not hold) fragment is an exception by constructing its finite Hilbert-style axiomatization. We also show that the monodic fragment with equality is not recursively axiomatizable.
---
paper_title: On the Completeness and Decidability of a Restricted First Order Linear Temporal Logic

paper_content:

The paper describes a class of FC-sequents of a restricted first order linear temporal logic with “next” and “always”. It is shown that the first order linear temporal logic is finitary complete for FC-sequents. If FC-sequents are logically decidable, i.e., all sequents, constructed from all possible subformulas of logical formulas of FC-sequents are decidable in first-order logic, then FC-sequents are decidable in the restricted first order linear temporal logic. To obtain these results a saturation calculus [6, 7] for FC-sequents is constructed.
---
paper_title: Decidable fragments of first-order temporal logics

paper_content:

Abstract In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps.
---
paper_title: Practical First-Order Temporal Reasoning

paper_content:

In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification.
---
paper_title: Monodic fragments of first-order temporal logics: 2000-2001 A.D

paper_content:

The aim of this paper is to summarize and analyze some results obtained in 2000-2001 about decidable and undecidable fragments of various first-order temporal logics, give some applications in the field of knowledge representation and reasoning, and attract the attention of the 'temporal community' to a number of interesting open problems.
---
paper_title: The Classical Decision Problem

paper_content:

1. Introduction: The Classical Decision Problem.- 1.1 The Original Problem.- 1.2 The Transformation of the Classical Decision Problem.- 1.3 What Is and What Isn't in this Book.- I. Undecidable Classes.- 2. Reductions.- 2.1 Undecidability and Conservative Reduction.- 2.1.1 The Church-Turing Theorem and Reduction Classes.- 2.1.2 Trakhtenbrot's Theorem and Conservative Reductions.- 2.1.3 Inseparability and Model Complexity.- 2.2 Logic and Complexity.- 2.2.1 Propositional Satisfiability.- 2.2.2 The Spectrum Problem and Fagin's Theorem.- 2.2.3 Capturing Complexity Classes.- 2.2.4 A Decidable Prefix-Vocabulary Class.- 2.3 The Classifiability Problem.- 2.3.1 The Problem.- 2.3.2 Well Partially Ordered Sets.- 2.3.3 The Well Quasi Ordering of Prefix Sets.- 2.3.4 The Well Quasi Ordering of Arity Sequences.- 2.3.5 The Classifiability of Prefix-Vocabulary Sets.- 2.4 Historical Remarks.- 3. Undecidable Standard Classes for Pure Predicate Logic.- 3.1 The Kahr Class.- 3.1.1 Domino Problems.- 3.1.2 Formalization of Domino Problems by $$[\forall \exists \forall , (0,\omega )]$$-Formulae.- 3.1.3 Graph Interpretation of $$[\forall \exists \forall , (0,\omega )]$$-Formulae.- 3.1.4 The Remaining Cases Without $$\exists *$$.- 3.2 Existential Interpretation for $$[{{\forall }^{3}}\exists *, (0,1)]$$.- 3.3 The Gurevich Class.- 3.3.1 The Proof Strategy.- 3.3.2 Reduction to Diagonal-Freeness.- 3.3.3 Reduction to Shift-Reduced Form.- 3.3.4 Reduction toFi-Elimination Form.- 3.3.5 Elimination of MonadicFi.- 3.3.6 The Kostyrko-Genenz and Suranyi Classes.- 3.4 Historical Remarks.- 4. Undecidable Standard Classes with Functions or Equality.- 4.1 Classes with Functions and Equality.- 4.2 Classes with Functions but Without Equality.- 4.3 Classes with Equality but Without Functions: the Goldfarb Classes 161 4.3.1 Formalization of Natural Numbers in $$[{{\forall }^{3}}\exists *, (\omega ,\omega ),(0)]$$=.- 4.3.2 Using Only One Existential Quantifiers.- 4.3.3 Encoding the Non-Auxiliary Binary Predicates.- 4.3.4 Encoding the Auxiliary Binary Predicates of NUM*.- 4.4 Historical Remarks.- 5. Other Undecidable Cases.- 5.1 Krom and Horn Formulae.- 5.1.1 Krom Prefix Classes Without Functions or Equality.- 5.1.2 Krom Prefix Classes with Functions or Equality.- 5.2 Few Atomic Subformulae.- 5.2.1 Few Function and Equality Free Atoms.- 5.2.2 Few Equalities and Inequalities.- 5.2.3 Horn Clause Programs With One Krom Rule.- 5.3 Undecidable Logics with Two Variables.- 5.3.1 First-Order Logic with the Choice Operator.- 5.3.2 Two-Variable Logic with Cardinality Comparison.- 5.4 Conjunctions of Prefix-Vocabulary Classes.- 5.4.1 Reduction to the Case of Conjunctions.- 5.4.2 Another Classifiability Theorem.- 5.4.3 Some Results and Open Problems.- 5.5 Historical Remarks.- II. Decidable Classes and Their Complexity.- 6. Standard Classes with the Finite Model Property.- 6.1 Techniques for Proving Complexity Results.- 6.1.1 Domino Problems Revisited.- 6.1.2 Succinct Descriptions of Inputs.- 6.2 The Classical Solvable Cases.- 6.2.1 Monadic Formulae.- 6.2.2 The Bernays-Schonfinkel-Ramsey Class.- 6.2.3 The Godel-Kalmar-Schutte Class: a Probabilistic Proof.- 6.3 Formulae with One ?.- 6.3.1 A Satisfiability Test for [?*??*, all, all].- 6.3.2 The Ackermann Class.- 6.3.3 The Ackermann Class with Equality.- 6.4 Standard Classes of Modest Complexity.- 6.4.1 The Relational Classes in P, NP and Co-NP.- 6.4.2 Fragments of the Theory of One Unary Function.- 6.4.3 Other Functional Classes.- 6.5 Finite Model Property vs. Infinity Axioms.- 6.6 Historical Remarks.- 7. Monadic Theories and Decidable Standard Classes with Infinity Axioms.- 7.1 Automata, Games and Decidability of Monadic Theories.- 7.1.1 Monadic Theories.- 7.1.2 Automata on Infinite Words and the Monadic Theory of One Successor.- 7.1.3 Tree Automata, Rabin's Theorem and Forgetful De terminacy.- 7.1.4 The Forgetful Determinacy Theorem for Graph Games.- 7.2 The Monadic Second-Order Theory of One Unary Function.- 7.2.1 Decidability Results for One Unary Function.- 7.2.2 The Theory of One Unary Function is not Elementary Recursive.- 7.3 The Shelah Class.- 7.3.1 Algebras with One Unary Operation.- 7.3.2 Canonic Sentences.- 7.3.3 Terminology and Notation.- 7.3.4 1-Satisfiability.- 7.3.5 2-Satisfiability.- 7.3.6 Refinements.- 7.3.7 Villages.- 7.3.8 Contraction.- 7.3.9 Towns.- 7.3.10 The Final Reduction.- 7.4 Historical Remarks.- 8. Other Decidable Cases.- 8.1 First-Order Logic with Two Variables.- 8.2 Unification and Applications to the Decision Problem.- 8.2.1 Unification.- 8.2.2 Herbrand Formulae.- 8.2.3 Positive First-Order Logic.- 8.3 Decidable Classes of Krom Formulae.- 8.3.1 The Chain Criterion.- 8.3.2 The Aanderaa-Lewis Class.- 8.3.3 The Maslov Class.- 8.4 Historical Remarks.- A. Appendix: Tiling Problems.- A.1 Introduction.- A.2 The Origin Constrained Domino Problem.- A.3 Robinson's Aperiodic Tile Set.- A.4 The Unconstrained Domino Problem.- A.5 The Periodic Problem and the Inseparability Result.- Annotated Bibliography.
---
paper_title: Many-Dimensional Modal Logics: Theory and Applications

paper_content:

I Introduction 1 Modal logic basics 1.1 Modal axiomatic systems 1.2 Possible world semantics 1.3 Classical first-order logic and the standard translation 1.4 Multimodal logics 1.5 Algebraic semantics 1.6 Decision, complexity and axiomatizability problems 2 Applied modal logic 2.1 Temporal logic 2.2 Interval temporal logic 2.3 Epistemic logic 2.4 Dynamic logic 2.5 Description logic 2.6 Spatial logic 2.7 Intuitionistic logic 2.8 'Model level' reductions between logics 3 Many-dimensional modal logics 3.1 Fusions 3.2 Spatio-temporal logics 3.3 Products 3.4 Temporal epistemic logics 3.5 Classical first-order logic as a propositional multimodal logic 3.6 First-order modal logics 3.7 First-order temporal logics 3.8 Description logics with modal operators 3.9 HS as a two-dimensional logic 3.10 Modal transition logics 3.11 Intuitionistic modal logics II Fusions and products 4 Fusions of modal logics 4.1 Preserving Kripke completeness and the finite model property 4.2 Algebraic preliminaries 4.3 Preserving decidability of global consequence 4.4 Preserving decidability 4.5 Preserving interpolation 4.6 On the computational complexity of fusions 5 Products of modal logics: introduction 5.1 Axiomatizing products 5.2 Proving decidability with quasimodels 5.3 The finite model property 5.4 Proving undecidability 5.5 Proving complexity with tilings 6 Decidable products 6.1 Warming up: Kn x Km 6.2 CPDL x K_m 6.3 Products of epistemic logics with Km 6.4 Products of temporal logics with Km 6.5 Products with S5 6.6 Products with multimodal S5 7 Undecidable products 7.1 Products of linear orders with infinite ascending chains 7.2 Products of linear orders with infinite descending chains 7.3 Products of Dedekind complete linear orders 7.4 Products of finite linear orders 7.5 More undecidable products 8 Higher-dimensional products 8.1 S5 x S5 x ... x S5 8.2 Products between K4 x K4 x ... x K4 and S5 x S5 x ... x S5 8.3 Products with the fmp 8.4 Between K x K x ... x K and S5 x S5 x ... x S5 8.5 Finitely axiomatizable and decidable products 9 Variations on products 9.1 Relativized products 9.2 Valuation restrictions 10 Intuitionistic modal logics 10.1 Intuitionistic modal logics with Box 10.2 Intuitionistic modal logics with Box and Diamond 10.3 The finite model property III First-order modal logics 11 Fragments of first-order temporal logics 11.1 Undecidable fragments 11.2 Monodic formulas, decidable fragments 11.3 Embedding into monadic second-order theories 11.4 Complexity of decidable fragments of QLogSU(N) 11.5 Satisfiability in models over (N,<) with finite domains 11.6 Satisfiability in models over (R,<) with finite domains 11.7 Axiomatizing monodic fragments 11.8 Monodicity and equality 12 Fragments of first-order dynamic and epistemic logics 12.1 Decision problems 12.2 Axiomatizing monodic fragments IV Applications to knowledge representation 13 Temporal epistemic logics 13.1 Synchronous systems 13.2 Agents who know the time and neither forget nor learn 14 Modal description logics 14.1 Concept satisfiability 14.2 General formula satisfiability 14.3 Restricted formula satisfiability 14.4 Satisfiability in models with finite domains 15 Tableaux for modal description logics 15.1 Tableaux for ALC 15.2 Tableaux for K(ALC) with constant domains 15.3 Adding expressive power to K(ALC) 16 Spatio-temporal logics 16.1 Modal formalisms for spatio-temporal reasoning 16.2 Embedding spatio-temporal logics in first-order temporal logic 16.3 Complexity of spatio-temporal logics 16.4 Models based on Euclidean spaces Epilogue. Bibliography. List of tables. List of languages and logics. Symbol index. Subject index.
---
paper_title: Equality and Monodic First-Order Temporal Logic

paper_content:

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.
---
paper_title: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

paper_content:

We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
---
paper_title: A temporal logic for reasoning about processes and plans

paper_content:

Much previous work in artificial intelligence has neglected representing time in all its complexity. In particular, it has neglected continuous change and the indeterminacy of the future. To rectify this, I have developed a first-order temporal logic, in which it is possible to name and prove things about facts, events, plans, and world histories. In particular, the logic provides analyses of causality, continuous change in quantities, the persistence of facts (the frame problem), and the relationship between tasks and actions. It may be possible to implement a temporal-inference machine based on this logic, which keeps track of several “maps” of a time line, one per possible history.
---
paper_title: The temporal logic of branching time

paper_content:

A temporal language and system are presented which are based on branching time structure. By the introduction of symmetrically dual sets of temporal operators, it is possible to discuss properties which hold either along one path or along all paths. Consequently it is possible to express in this system all the properties that were previously expressible in linear time or branching time systems. We present an exponential decision procedure for satisfiability in the language based on tableaux methods, and a complete deduction system. As associated temporal semantics is illustrated for both structured and graph representation of programs.
---
paper_title: Formal methods for the specification and design of real-time safety critical systems

paper_content:

Abstract Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies that fail to meet stringent timing constraints have resulted in catastrophic failures. This article surveys formal methods for specifying, designing, and verifying real-time systems so as to improve their safety and reliability.
---
paper_title: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

paper_content:

The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.
---
paper_title: A Model-Theoretic Approach to the Verification of Situated Reasoning Systems

paper_content:

The study of situated systems that are capable of reactive and goal-directed behaviour has received increased attention in recent years. One approach to the design of such systems is based upon agent-oriented architectures. This approach has led to the development of expressive, but computationally intractable, logics for describing or specifying the behaviours of agent-oriented systems. In this paper, we present three propositional variants of such logics, with different expressive power, and analyze the computational complexity of verifying if a given property is satisfied by a given abstract agent-oriented system. We show the complexity to be linear time for one of these logics and polynomial time for another, thus providing encouraging results with respect to the practical use of such logics for verifying agent-oriented systems.
---
paper_title: A Hierarchy of Temporal Logics with Past

paper_content:

We extend the classical hierarchy of branching-time temporal logics between UB and CTL* by studying which additional expressive power (if any) stems from the incorporation of past-time modalities. In addition, we propose a new temporal combinator, N for “Now”, that brings new and interesting expressive power. In several situations, non-trivial translation algorithms exist from a temporal logic with past to a pure-future fragment. These algorithms have important practical applications e.g. in the field of model-checking.
---
paper_title: Counting CTL

paper_content:

This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and succinctness, and of the complexity of their model-checking and satisfiability problems (ranging from P-complete to undecidable). Finally, we present two alternative logics with similar features and provide a comparative study of the properties of both variants.
---
paper_title: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time

paper_content:

We consider the computation tree logic (CTL) proposed in (Sci. Comput. Programming 2 (1982), 241–260) which extends the unified branching time logic (UB) of (“Proc. Ann. ACM Sympos. Principles of Programming Languages, 1981,” pp. 164–176) by adding an until operator. It is established that CTL has the small model property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from the small “pseudomodel” resulting from the Fischer-Ladner quotient construction. Then an exponential time algorithm is given for deciding satisfiability in CTL, and the axiomatization of UB given in ibid. is extended to a complete axiomatization for CTL. Finally, the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL is studied.
---
paper_title: Using branching time temporal logic to synthesize synchronization skeletons

paper_content:

Abstract We present a method of constructing concurrent programs in which the synchronization skeleton of the program is automatically synthesized from a (branching time) temporal logic specification. The synthesis method uses a decision procedure based on the finite model property of the logic to determine satisfiability of the specification formula f. If f is satisfiable, then a model for f with a finite number of states is constructed. The synchronization skeleton of a program meeting the specification can be read from this model. If f is unsatisfiable, the specification is inconsistent.
---
paper_title: Branching time temporal logic

paper_content:

Many important parallel computer programs exhibit ongoing behaviour that is characterized naturally in terms of infinite execution traces, which can be organized into “branching” trees, and which reflect the high degree of nondeterminism inherent in parallel computation. In this paper, we give a systematic account of Branching Time Temporal Logics, which provide a formal system for describing and reasoning about the correct behaviour of such programs. Several systems of branching time temporal logic that have appeared in the literature are presented, and significant related issues such as their axiomatizations, and decision procedures for their satisfiability and model checking problems are discussed. The applicability of their axiomatizations to formulate deductive systems of these temporal logics to reason about the correctness of concurrent programs is then described as is that of their decision procedures to the tasks of mechanical synthesis and verification. A comparison of the relative expressive power of these systems of branching time temporal logic is also presented, and their ability to specify important correctness properties of programs, including those that involve fairness, is discussed. Moreover, their expressiveness is related to both, the expressiveness of corresponding linear time temporal logics, as well as that of other standard formalisms such as the monadic second-order theory of many successors and finite-state tree automata. Finally, a comparison is undertaken between branching time temporal logics and linear time ones, particularly with respect to their adequacy for such applications as specifying and reasoning about the correctness of concurrent programs.
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

paper_content:

The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.
---
paper_title: The Complexity of Tree Automata and Logics of Programs

paper_content:

The complexity of testing nonemptiness of finite state automata on infinite trees is investigated. It is shown that for tree automata with the pairs (or complemented pairs) acceptance condition having m states and n pairs, nonemptiness can be tested in deterministic time (mn)O(n); however, it is shown that the problem is in general NP-complete (or co-NP-complete, respectively). The new nonemptiness algorithm yields exponentially improved, essentially tight upper bounds for numerous important modal logics of programs, interpreted with the usual semantics over structures generated by binary relations. For example, it follows that satisfiability for the full branching time logic CTL* can be tested in deterministic double exponential time. Another consequence is that satisfiability for propositional dynamic logic (PDL) with a repetition construct (PDL-delta) and for the propositional Mu-calculus ($L\mu$) can be tested in deterministic single exponential time.
---
paper_title: An axiomatization of full Computation Tree Logic

paper_content:

We give a sound and complete axiomatization for the full computation tree logic, CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: An axiomatization of PCTL*

paper_content:

A sound and complete axiomatization for a computation tree logic with past operators, PCTL*, is given. The logic extends the standard branching time logic CTL* of R-generable models via the use of past time operators and semantics based on a finite linear past leading back from any point in any fullpath. Furthermore, the valid formulas of CTL* are also valid in PCTL*. The past operators allow us to avoid use of any unusual rules of inference such as the ugly automata-motivated AA rule which is part of the existing complete axiomatization for CTL*.
---
paper_title: A Hierarchy of Temporal Logics with Past

paper_content:

We extend the classical hierarchy of branching-time temporal logics between UB and CTL* by studying which additional expressive power (if any) stems from the incorporation of past-time modalities. In addition, we propose a new temporal combinator, N for “Now”, that brings new and interesting expressive power. In several situations, non-trivial translation algorithms exist from a temporal logic with past to a pure-future fragment. These algorithms have important practical applications e.g. in the field of model-checking.
---
paper_title: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time

paper_content:

We consider the computation tree logic (CTL) proposed in (Sci. Comput. Programming 2 (1982), 241–260) which extends the unified branching time logic (UB) of (“Proc. Ann. ACM Sympos. Principles of Programming Languages, 1981,” pp. 164–176) by adding an until operator. It is established that CTL has the small model property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from the small “pseudomodel” resulting from the Fischer-Ladner quotient construction. Then an exponential time algorithm is given for deciding satisfiability in CTL, and the axiomatization of UB given in ibid. is extended to a complete axiomatization for CTL. Finally, the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL is studied.
---
paper_title: Temporal logic : mathematical foundations and computational aspects

paper_content:

1. The handling of time: introduction and survey 2. Semantical presentation of temporal connectives 3. Axiomatic presentation of propositional temporal connectives 4. Predicate temporal logics 5. Temporal logics presented in the predicate calculus: language-metalanguage 6. A general theory of axiomatization for propositional temporal logic 7. Basic many-dimensional systems 8. Propositional quantifiers and fixed point operators 9. Expressive power of one-dimensional temporal connectives: basic concepts 10. Expressive completeness of Since and Until over integer and real time 11. Expressive completeness of Stavi connectives over general linear time 12. Further expressive completeness results 13. H-dimension 14. Adding a temporal dimension to a logic system 15. Decidability in temporal logic Bibliography Notation Index Index of Systems Index
---
paper_title: Using branching time temporal logic to synthesize synchronization skeletons

paper_content:

Abstract We present a method of constructing concurrent programs in which the synchronization skeleton of the program is automatically synthesized from a (branching time) temporal logic specification. The synthesis method uses a decision procedure based on the finite model property of the logic to determine satisfiability of the specification formula f. If f is satisfiable, then a model for f with a finite number of states is constructed. The synchronization skeleton of a program meeting the specification can be read from this model. If f is unsatisfiable, the specification is inconsistent.
---
paper_title: Compositional temporal logic based on partial order

paper_content:

The temporal logic of distributed actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.
---
paper_title: Adding partial orders to linear temporal logic

paper_content:

Modeling execution as partial orders increases the flexibility in reasoning about concurrent programs by allowing the use of alternative, equivalent execution sequences. This is a desirable feature in specifying concurrent systems which allows formalizing frequently used arguments such as ‘in an equivalent execution sequence’, or ‘in a consistent global state, not necessarily on the execution sequence’ to be formalized. However, due to the addition of structure to the model, verification of partial order properties is non-trivial and sparse. We present here a new approach which allows expressing and verifying partial order properties. It is based on modeling an execution as a linear sequence of global states, where each state is equipped with its past partial-order history. The temporal logic BPLTL (for Branching Past Linear Temporal Logic) is introduced. We provide a sound and relatively complete proof system for the logic BPLTL over transitions programs. Our proof system augments an existing proof system for LTL.
---
paper_title: A temporal logic for reasoning about partially ordered computations (Extended Abstract)

paper_content:

Current Temporal Logics are all oriented towards the description of totally ordered sequences. This limits their usefulness for reasoning about systems whose computations cannot easily be mapped into totally ordered sequences. Here, we propose a temporal logic geared towards describing partially ordered sets and apply it to dynamic distributed systems. Even though the logic we define does not have the finite model property, we establish that it has a one exponential decision procedure and a complete axiomatization.
---
paper_title: Multi-Dimensional Modal Logic

paper_content:

We start with informally defining the subject matter of this book: multi-dimensional modal logic (MDML). First let us briefly consider what we understand by the notion of “modal logic”. The last decade has seen a development in modal logic towards a more abstract and technical approach. In this perspective of what one might call abstract modal logic, arbitrary relational structures can be seen as models for an (extended) modal language: any relation is a potential accessibility relation of some suitably defined modal operator. As the essentially modal aspect of the framework one could point out that the mechanism for evaluating formulas forces certain moves along the accessibility relations. Thus, for instance quantification over a model is restricted to an “accessible” part of the structure.
---
paper_title: Undecidability of Compass Logic

paper_content:

It is known that the tiling technique can be used to give simple proofs of undecidability of various two-dimensional modal and temporal logics. However, up until now, the simplest two-dimensional temporal logic, the compass logic of Venema, has eluded such treatment. We present a new coding of an enumeration of the tiling plane which enables us to show that the compass logic is undecidable.
---
paper_title: A general tableau method for propositional interval temporal logics

paper_content:

Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various 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 temporal logics. In this paper, we introduce a new, very expressive propositional interval temporal logic, called (Non-Strict) Branching CDT (BCDT + ) which extends most of the propositional interval temporal logics proposed in the literature. Then, we provide BCDT + with a generic tableau method which combines features of explicit tableau methods for modal logics with constraint label management and the classical tableau method for first-order logic, and we prove its soundness and completeness.
---
paper_title: A tableau-based decision procedure for right propositional neighborhood logic

paper_content:

Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most such logics turned out to be (highly) undecidable. To get decidability, severe syntactic and/or semantic restrictions have been imposed to interval-based temporal logics that make it possible to reduce them to point-based ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones which are genuinely interval-based is still largely unexplored. In this paper, we make one step in this direction by devising an original tableau-based decision procedure for the future fragment of Propositional Neighborhood Interval Temporal Logic, interpreted over natural numbers.
---
paper_title: On Decidability and Expressiveness of Propositional Interval Neighborhood Logics

paper_content:

Interval-based temporal logics are an important research area in computer science and artificial intelligence. In this paper we investigate decidability and expressiveness issues for Propositional Neighborhood Logics (PNLs). We begin by comparing the expressiveness of the different PNLs. Then, we focus on the most expressive one, namely, PNL?+, and we show that it is decidable over various classes of linear orders by reducing its satisfiability problem to that of the two-variable fragment of first-order logic with binary relations over linearly ordered domains, due to Otto. Next, we prove that PNL?+is expressively complete with respect to such a fragment. We conclude the paper by comparing PNL?+expressiveness with that of other interval-based temporal logics.
---
paper_title: An optimal Tableau-based decision algorithm for propositional neighborhood logic

paper_content:

In this paper we focus our attention on the decision problem for Propositional Neighborhood Logic (PNL for short). PNL is the proper subset of Halpern and Shoham's modal logic of intervals whose modalities correspond to Allen's relations meets and met by. We show that the satisfiability problem for PNL over the integers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure and we prove its optimality.
---
paper_title: Decidability of the Logics of the Reflexive Sub-interval and Super-interval Relations over Finite Linear Orders

paper_content:

An interval temporal logic is a propositional, multi-modal logic interpreted over interval structures of partial orders. The semantics of each modal operator are given in the standard way with respect to one of the natural accessibility relations defined on such interval structures. In this paper, we consider the modal operators based on the (reflexive) sub-interval relation and the (reflexive) super-interval relation. We show that the satisfiability problems for the interval temporal logics featuring either or both of these modalities, interpreted over interval structures of finite linear orders, are all PSPACE-complete. These results fill a gap in the known complexity results for interval temporal logics.
---
paper_title: A Decidable Temporal Logic for Events and States

paper_content:

This paper introduces a new interval temporal logic, TPL*. Existing interval temporal logics, we claim, are inadequate to represent the meanings of certain natural language constructions, despite exhibiting high computational complexity. TPL* overcomes these problems, presents the semantics of some natural language constructions, and captures important real-time problems like behaviour of complex systems
---
paper_title: Temporal prepositions and their logic

paper_content:

A fragment of English featuring temporal prepositions and the order-denoting adjectives first and last is defined by means of a context-free grammar. The phrase-structures which this grammar assigns to the sentences it recognizes are viewed as formulas of an interval temporal logic, whose satisfaction-conditions faithfully represent the meanings of the corresponding English sentences. It is shown that the satisfiability problem for this logic is NEXPTIME-complete. The computational complexity of determining logical relationships between English sentences featuring the temporal constructions in question is thus established.
---
paper_title: Tableaux for Logics of Subinterval Structures over Dense Orderings

paper_content:

In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.
---
paper_title: Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions

paper_content:

Abstract In this paper, we investigate the expressiveness of the variety of propositional interval neighborhood logics (PNL), we establish their decidability on linearly ordered domains and some important subclasses, and we prove the undecidability of a number of extensions of PNL with additional modalities over interval relations. All together, we show that PNL form a quite expressive and nearly maximal decidable fragment of Halpern–Shoham’s interval logic HS.
---
paper_title: A calculus of durations

paper_content:

Abstract The purpose of the calculus of durations is to reason about designs and requirements for time-critical systems, without explicit mention of absolute time. Its distinctive feature is reasoning about integrals of the durations of different states within any given interval. The first section introduces the running example, of leakage in a gas burner. The second section defines and axiomatises the proposed calculus as an extension of interval temporal logic. The third section applies it to the problem described in the introduction. The fourth section briefly surveys alternative calculi.
---
paper_title: Reasoning About Digital Circuits

paper_content:

Abstract : Predicate logic is a powerful and general descriptive formalism with a long history of development. However, since the logic's underlying semantics have no notion of time, statements such as I increases by 2 and The bit signal X rises from 0 to 1 can not be directly expressed. The author presents a formalism called interval temporal logic (ITL) that augments standard predicate logic with time-dependent operators. ITL is like discrete linear-time temporal logic but includes time intervals. The behavior of programs and hardware devices can often be decomposed into successively smaller intervals of activity. State transitions can be characterized by properties relating the initial and final values of variables over intervals. Furthermore, these time periods provide a convenient framework for introducing quantitative timing details. After giving some motivation for reasoning about hardware, he presents the propositional and first-order syntax and semantics of ITL. Demonstrated is ITL's utility for uniformly describing the structure and dynamics of a wide variety of timing-dependent digital circuits. Devices discussed include delay elements, adders, latches, flip-flops, counters, random-access memories, a clocked multiplication circuit and the Am2901 bit slice. ITL also provides a means for expressing properties of such specifications. Also examine are such concepts as device equivalence and internal states. Propositional ITL is shown to be undecidable although useful subsets are of relatively reasonable computational complexity. (Author)
---
paper_title: A complete axiomatization of interval temporal logic with infinite time

paper_content:

Interval Temporal Logic (ITL) is a formalism for reasoning about time periods. To date no one has proved completeness of a relatively simple ITL deductive system supporting infinite time and permitting infinite sequential iteration comparable to ω -regular expressions. We give a complete axiomatization for such a version of quantified ITL over finite domains and can show completeness by representing finite-state automata in ITL and then translating ITL formulas into them. The full paper (and another conference paper) presents the basic framework for finite time. Here and in the full paper the axiom system (and completeness) is extended to infinite time.
---
paper_title: A calculus of durations

paper_content:

Abstract The purpose of the calculus of durations is to reason about designs and requirements for time-critical systems, without explicit mention of absolute time. Its distinctive feature is reasoning about integrals of the durations of different states within any given interval. The first section introduces the running example, of leakage in a gas burner. The second section defines and axiomatises the proposed calculus as an extension of interval temporal logic. The third section applies it to the problem described in the introduction. The fourth section briefly surveys alternative calculi.
---
paper_title: Take It NP-Easy: Bounded Model Construction for Duration Calculus

paper_content:

Following the recent successes of bounded model-checking, we reconsider the problem of constructing models of discrete-time Duration Calculus formulae. While this problem is known to be nonelementary when arbitrary length models are considered [Han94], it turns out to be only NP-complete when constrained to bounded length.As a corollary we obtain that model construction is in NP for the formulae actually encountered in case studies using Duration Calculus, as these have a certain small-model property.First experiments with a prototype implementation of the procedures demonstrate a competitive performance.
---
paper_title: Verifying Linear Duration Constraints of Timed Automata

paper_content:

This paper aims at developing a technique for checking if a timed automaton satisfies a linear duration constraint on the automaton states. The constraints are represented in the form of linear duration invariants - a simple class of chop-free Duration Calculus (DC) formulas. We prove that linear duration invariants of timed automata are discretisable, and reduce checking if a timed automaton satisfies a linear duration invariant to checking if the integer timed region graph of the original automaton satisfies the same linear duration invariant. The latter can be done with exhaustive search on graphs. In comparison to the techniques in the literature, our method is more powerful: it works for the standard semantics of DC and the class of the closed timed automata while the others cannot be applied.
---
paper_title: Maintaining knowledge about temporal intervals

paper_content:

An interval-based temporal logic is introduced, together with a computationally effective reasoning algorithm based on constraint propagation. This system is notable in offering a delicate balance between
---
paper_title: Linear Duration Invariants

paper_content:

This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time systems in the paper are taken to be real-time automata which set up for each of state transitions a lower time bound and an upper time bound. The satisfaction problem can be translated into a family of linear programming problems. The algorithm is, according to the invariants, to reduce the infinite family of linear programming problems to an equivalent one with only finite members, and then to solve each of linear programming problems efficiently. The algorithm is so simple that no prerequisite of linear programming theory is assumed.
---
paper_title: Symbolic model checking without BDDs

paper_content:

Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stalmarck's Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability. We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.
---
paper_title: Some Decidability Results for Duration Calculus under Synchronous Interpretation

paper_content:

Duration Calculus (or DC in short) presents a formal notation to specify properties of real-time systems and a calculus to formally prove such properties. Decidability is the underlying foundation to automated reasoning. But, excepting some of its simple fragments, DC has been shown to be undecidable.
---
paper_title: Deciding an Interval Logic with Accumulated Durations

paper_content:

A decidability result and a model-checking procedure for a rich subset of Duration Calculus (DC) [19] is obtained through reductions to first-order logic over the real-closed field and to Multi-Priced Timed Automata (MPTA) [13]. In contrast to other reductions of fragments of DC to reachability problems in timed automata, the reductions do also cover constraints on positive linear combinations of accumulated durations. By being able to handle accumulated durations under chop as well as in arbitrary positive Boolean contexts, the procedures extend the results of Zhou et al. [22] on decidability of linear duration invariants to a much wider fragment of DC.
---
paper_title: Duration Calculus: A Formal Approach to Real-Time Systems

paper_content:

The Duration Calculus (DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses real numbers to model time, and Boolean-valued (i.e. 0, 1-valued) functions over time to model states of real-time systems. The duration of a state in a time interval is the accumulated presence time of the state in the interval. DC extends interval logic with a calculus to specify and reason about properties of state durations. The first paper of DC was published in 1991, and dozens of papers of DC have been published since then, which cover developments of logical calculi, their applications and mechanical support tools. This paper will give a brief introduction to DC and also an overview of the research of DC.
---
paper_title: A calculus of durations

paper_content:

Abstract The purpose of the calculus of durations is to reason about designs and requirements for time-critical systems, without explicit mention of absolute time. Its distinctive feature is reasoning about integrals of the durations of different states within any given interval. The first section introduces the running example, of leakage in a gas burner. The second section defines and axiomatises the proposed calculus as an extension of interval temporal logic. The third section applies it to the problem described in the introduction. The fourth section briefly surveys alternative calculi.
---
paper_title: Checking Linear Duration Invariants by Linear Programming

paper_content:

In this paper, the problem of verifying a timed automaton for a Duration Calculus formula in the form of linear duration invariants
---
paper_title: ICS: Integrated Canonizer and Solver

paper_content:

Decision procedures are at the core of many industrial-strength verification systems such as ACL2 [KM97], PVS [ORS92], or STeP [MtSg96]. Effective use of decision procedures in these verification systems require the management of large assertional contexts. Many existing decision procedures, however, lack an appropriate API for managing contexts and efficiently switching between contexts, since they are typically used in a fire-and-forget environment.
---
paper_title: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

paper_content:

Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. Uppaal also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.
---
paper_title: Bounded validity checking of interval duration logic

paper_content:

A rich dense-time logic, called Interval Duration Logic (IDL), is useful for specifying quantitative properties of timed systems. The logic is undecidable in general. However, several approaches can be used for checking validity (and model checking) of IDL formulae in practice. In this paper, we propose bounded validity checking of IDL formulae by polynomially reducing this to checking unsatisfiability of lin-sat formulae. We implement this technique and give performance results obtained by checking the unsatisfiability of the resulting lin-sat formulae using the ICS solver. We also perform experimental comparisons of several approaches for checking validity of IDL formulae, including (a) digitization followed by automata-theoretic analysis, (b) digitization followed by pure propositional SAT solving, and (c) lin-sat solving as proposed in this paper. Our experiments use a rich set of examples drawn from the Duration Calculus literature.
---
paper_title: Take It NP-Easy: Bounded Model Construction for Duration Calculus

paper_content:

Following the recent successes of bounded model-checking, we reconsider the problem of constructing models of discrete-time Duration Calculus formulae. While this problem is known to be nonelementary when arbitrary length models are considered [Han94], it turns out to be only NP-complete when constrained to bounded length.As a corollary we obtain that model construction is in NP for the formulae actually encountered in case studies using Duration Calculus, as these have a certain small-model property.First experiments with a prototype implementation of the procedures demonstrate a competitive performance.
---
paper_title: Automatic symbolic verification of embedded systems

paper_content:

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
---
paper_title: Digitizing Interval Duration Logic

paper_content:

In this paper, we study the verification of dense time properties by discrete time analysis. Interval Duration Logic, (IDL), is a highly expressive dense time logic for specifying properties of real-time systems. Validity checking of IDL formulae is in general undecidable. A corresponding discrete-time logic QDDC has decidable validity.
---
paper_title: Symbolic model checking without BDDs

paper_content:

Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stalmarck's Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce a bounded model checking procedure for LTL which reduces model checking to propositional satisfiability. We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.
---

Title: A Survey on Temporal Logics
Section 1: Introduction
Description 1: This section introduces the concept of temporal logics and discusses their significance in capturing state changes over time. It explains the aim of the paper and the scope of various temporal logics to be analyzed.

Section 2: Preliminaries
Description 2: This section outlines the main criteria for classifying temporal logics, providing an overview of point vs. interval structures, and linear vs. branching structures, among other properties.

Section 3: Propositional Temporal Logics
Description 3: This section covers the introduction of temporal operators into classical logic and discusses key developments in Linear Temporal Logic (LTL) and Propositional Temporal Logic (PTL), including important results on decidability and expressiveness.

Section 4: First-Order Temporal Logics
Description 4: This section explains the extension of propositional temporal logics to first-order temporal logics (FOTL), highlighting their high expressiveness and complexities, as well as various fragments developed to balance expressiveness with computational feasibility.

Section 5: Undecidable Fragments of QTL
Description 5: This section reviews fragments of first-order temporal logic (QTL) that are undecidable, discussing the inherent complexities and challenges that arise from specific features of the quantification types within these logics.

Section 6: Decidable Fragments of QTL
Description 6: This section discusses the decidable fragments of first-order temporal logic (QTL) that maintain decidability through specific constraints on the use of quantifiers and temporal operators.

Section 7: Branching Time Temporal Logics
Description 7: This section provides an overview of branching time logics, including Computational Tree Logic (CTL) and its extensions, CTL* and CTL*[P], emphasizing their applications and computational properties.

Section 8: Computational Tree Logic (CTL)
Description 8: This section provides an in-depth analysis of CTL, its syntax, semantics, expressiveness, and its efficient model checking algorithms.

Section 9: Full Computational Tree Logic (CTL*)
Description 9: This section discusses CTL*, its enhancements over CTL, impact on expressiveness, and the complexity of its satisfiability and model-checking problems.

Section 10: Full Computational Tree Logic with Past (CTL*[P])
Description 10: This section explores the introduction of past operators in CTL*, covering their theoretical implications and the resulting complete axiomatization.

Section 11: Expressiveness of Branching Temporal Logics
Description 11: This section examines the expressiveness of various branching temporal logics and their efficiency in model-checking tasks, highlighting some common properties and system specifications.

Section 12: Partial-Order Temporal Logics
Description 12: This section discusses logics that cater to partially ordered computations, suitable for concurrent systems, and introduces important logics like POTL and its extensions.

Section 13: Interval Temporal Logics
Description 13: This section introduces interval temporal logics, explaining their added expressiveness over point-based logics and discussing prominent examples of interval logics.

Section 14: Propositional Interval Temporal Logics
Description 14: This section presents well-known propositional interval temporal logics that utilize unary or binary modal operators, highlighting their expressiveness and applications.

Section 15: The Logic HS
Description 15: This section covers the logic HS, its expressive power, and the formal aspects that allow it to represent different temporal structures, along with its axiomatization and undecidability results.

Section 16: The Logic CDT
Description 16: This section explains the logic CDT, its expressiveness, and the sound and complete axiomatic systems associated with it, as well as its decidability issues.

Section 17: The Logic PNL
Description 17: This section provides an overview of Propositional Neighbourhood Logic (PNL), its expressive capabilities, axiomatic systems, and satisfiability problems.

Section 18: Subinterval Logics
Description 18: This section reviews the logics based on subinterval structures, discussing their computational complexity and recent decidability results.

Section 19: First-Order Interval Temporal Logics
Description 19: This section discusses first-order interval temporal logics like ITL, their extensions and applications, along with known axiomatic systems and undecidability results.

Section 20: The Logic ITL
Description 20: This section provides an in-depth analysis of ITL, its syntax, semantics, axiomatic systems, and various extensions for different application domains.

Section 21: The Logic NL
Description 21: This section explores the logic NL, its modalities, expressive power, and the associated axiomatic systems.

Section 22: The Logic DC
Description 22: This section discusses Duration Calculus (DC), its use in specifying real-time systems, axiomatic systems, various fragments, and model checking techniques.

Section 23: The Logic IDL
Description 23: This section covers Interval Duration Logic (IDL), its expressive syntax, applications in capturing real-time properties, and methods for dealing with its satisfiability and model checking problems.

Section 24: Conclusion
Description 24: This section summarizes the main findings of the survey, highlighting the important developments and comparisons of various temporal logics discussed throughout the paper.