Real-time and Probabilistic Temporal Logics: An Overview
---
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: 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: Logics and Models of Real Time: A Survey

paper_content:

We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification.
---
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 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: 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: 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: 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: 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: From State Machines to Temporal Logic: Specification Methods for Protocol Standards

paper_content:

This paper attempts to lend perspective to several different methods that have been employed for specifying computer communication protocols by comparing a spectrum of specification techniques. The paper characterizes specification languages such as state transition diagrams, variants of temporal logic approaches, and sequence expressions by the extent to Which information is encoded as properties of a single state versus properties of a history of the entire computation state sequence. Taking the prototypical alternating bit protocol as an example, each method is used to specify the requirements for the send process of the distributed system.
---
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: 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: 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: 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: 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: 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: 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: 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: 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: 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: Logics and Models of Real Time: A Survey

paper_content:

We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification.
---
paper_title: Quantitative temporal reasoning

paper_content:

A substantially large class of programs operate in distributed and real-time environments, and an integral part of their correctness specification requires the expression of time-critical properties that relate the occurrence of events of the system. We focus on the formal specification and reasoning about the correctness of such programs. We propose a system of temporal logic, RTCTL (Real-Time Computation Tree Logic), that allows the melding of qualitative temporal assertions together with real-time constraints to permit specification and reasoning at the twin levels of abstraction: qualitative and quantitative. We argue that many practically useful correctness properties of temporal systems, which need to express timing as an essential part of their functionality requirements, can be expressed in RTCTL. We develop a model-checking algorithm for RTCTL whose complexity is linear in the size of the RTCTL specification formula and in the size of the structure. We also present an essentially optimal, exponential time tableau-based decision procedure for the satisfiability of RTCTL formulae. Finally, we consider several variants and extensions of RTCTL for real-time reasoning.
---
paper_title: Model-Checking for Real-Time Systems

paper_content:

Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill. However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables.
---
paper_title: Logics and Models of Real Time: A Survey

paper_content:

We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification.
---
paper_title: Model Checking Timed Automata with One or Two Clocks

paper_content:

In this paper, we study model checking of timed automata (TAs), and more precisely we aim at finding efficient model checking for subclasses of TAs. For this, we consider model checking TCTL and TCTL ≤,≥ over TAs with one clock or two clocks. First we show that the reachability problem is NLOGSPACE-complete for one clock TAs (i.e. as complex as reachability in classical graphs) and we give a polynomial time algorithm for model checking TCTL ≤,≥ over this class of TAs. Secondly we show that model checking becomes PSPACE-complete for full TCTL over one clock TAs. We also show that model checking CTL (without any timing constraint) over two clock TAs is PSPACE-complete and that reachability is NP-hard.
---
paper_title: Polytime model checking for timed probabilistic computation tree logic

paper_content:

We consider the model checking problem for Timed Probabilistic Computation Tree Logic (TPCTL) introduced by H.A. Hansson and D. Jonsson, and studied in a recent book by H.A. Hansson [Han94]. The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in [Han94] that model checking for TPCTL has exponential time complexity, the latter being measured in terms of the size of formula, the size of transition system and the value of explicit time that appears in the formula. Besides that, [Han94] describes some polytime decidable classes, the proofs being rather voluminous. We show, by a short proof, that this model checking problem is polytime decidable in the general case. The proof is essentially based on results on the complexity of Markov decision processes.
---
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: 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: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
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: Explicit clock temporal logic

paper_content:

The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finite state programs (model checking). The expressive power of XCTL is compared with that of some other logics proposed for the expression of real time properties. It is shown that it is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic). >
---
paper_title: The temporal specification and verification of real-time systems

paper_content:

We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of reactive systems. ::: Semantics. We introduce the abstract computational model of timed transition systems as a conservative extension of traditional transition systems: qualitative fairness requirements are superseded by quantitative real-time constraints on the transitions. Digital clocks are introduced as observers of continuous real-time behavior. We justify our semantical abstractions by demonstrating that a wide variety of concrete real-time systems can be modeled adequately. ::: Specification. We present two conservative extensions of temporal logic that allow for the specification of timing constraints: while timed temporal logic provides access to time through a novel kind of time quantifier, metric temporal logic refers to time through time-bounded versions of the temporal operators. We justify our choice of specification languages by developing a general framework for the classification of real-time logics according to their complexity and expressive power. ::: Verification. We develop tools for determining if a real-time system that is modeled as a timed transition system meets a specification that is given in timed temporal logic or in metric temporal logic. We present both model-checking algorithms for the automatic verification of finite-state real-time systems and proof methods for the deductive verification of real-time systems. Both techniques are conservative generalizations of the corresponding conventional approaches to program verification, which abstract time from consideration.
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
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: On the decidability of metric temporal logic

paper_content:

Metric temporal logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL-which includes invariance and time-bounded response properties-is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature. The question of the decidability of MTL over infinite words remains open.
---
paper_title: The temporal specification and verification of real-time systems

paper_content:

We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of reactive systems. ::: Semantics. We introduce the abstract computational model of timed transition systems as a conservative extension of traditional transition systems: qualitative fairness requirements are superseded by quantitative real-time constraints on the transitions. Digital clocks are introduced as observers of continuous real-time behavior. We justify our semantical abstractions by demonstrating that a wide variety of concrete real-time systems can be modeled adequately. ::: Specification. We present two conservative extensions of temporal logic that allow for the specification of timing constraints: while timed temporal logic provides access to time through a novel kind of time quantifier, metric temporal logic refers to time through time-bounded versions of the temporal operators. We justify our choice of specification languages by developing a general framework for the classification of real-time logics according to their complexity and expressive power. ::: Verification. We develop tools for determining if a real-time system that is modeled as a timed transition system meets a specification that is given in timed temporal logic or in metric temporal logic. We present both model-checking algorithms for the automatic verification of finite-state real-time systems and proof methods for the deductive verification of real-time systems. Both techniques are conservative generalizations of the corresponding conventional approaches to program verification, which abstract time from consideration.
---
paper_title: Alternating timed automata

paper_content:

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages that is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is nonprimitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock. We investigate extension of the model with epsilon-transitions and prove that emptiness is undecidable. Over infinite words, we show undecidability of the universality problem.
---
paper_title: The benefits of relaxing punctuality

paper_content:

The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satistiability of timing constraints that are capable of expressing punctuality in this model, however, is known to be undecidable. We introduce a temporal language that can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics. Categories and Subject Descriptors: C.3 (Special-Purpose and Application-Based Systems)--real- time systems; D.2.1 (Software Engineeriogk Requirements/Specifications-languages; F.3.1 (Lugics and Meanings of ~rugmms): Specifying and Verifying and Reasoning about Programs-lo& of programs; mechanical verification; specification techniques; F.4.3 (Mathematical Logic and Formal Languages): Formal Languages-classes f decision problems
---
paper_title: Specifying real-time properties with metric temporal logic

paper_content:

This paper is motivated by the need for a formal specification method for real-time systems. In these systemsquantitative temporal properties play a dominant role. We first characterize real-time systems by giving a classification of such quantitative temporal properties. Next, we extend the usual models for temporal logic by including a distance function to measure time and analyze what restrictions should be imposed on such a function. Then we introduce appropriate temporal operators to reason about such models by turning qualitative temporal operators into (quantitative) metric temporal operators and show how the usual quantitative temporal properties of real-time systems can be expressed in this metric temporal logic. After we illustrate the application of metric temporal logic to real-time systems by several examples, we end this paper with some conclusions.
---
paper_title: Logics and Models of Real Time: A Survey

paper_content:

We survey logic-based and automata-based languages and techniques for the specification and verification of real-time systems. In particular, we discuss three syntactic extensions of temporal logic: time-bounded operators, freeze quantification, and time variables. We also discuss the extension of finite-state machines with clocks and the extension of transition systems with time bounds on the transitions. All of the resulting notations can be interpreted over a variety of different models of time and computation, including linear and branching time, interleaving and true concurrency, discrete and continuous time. For each choice of syntax and semantics, we summarize the results that are known about expressive power, algorithmic finite-state verification, and deductive verification.
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
paper_title: STATEMATE: a working environment for the development of complex reactive systems

paper_content:

This paper provides a brief overview of the STATEMATE system, constructed over the past three years by i-Logix Inc., and Ad Cad Ltd. STATEMATE is a graphical working environment, intended for the specification, analysis, design and documentation of large and complex reactive systems, such as real-time embedded systems, control and communication systems, and interactive software. It enables a user to prepare, analyze and debug diagrammatic, yet precise, descriptions of the system under development from three inter-related points of view, capturing, structure, functionality and behavior . These views are represented by three graphical languages, the most intricate of which is the language of statecharts used to depict reactive behavior over time. In addition to the use of state-charts, the main novelty of STATEMATE is in the fact that it `understands` the entire descriptions perfectly, to the point of being able to analyze them for crucial dynamic properties, to carry out rigorous animated executions and simulations of the described system, and to create running code automatically. These features are invaluable when it comes to the quality and reliability of the final outcome.
---
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: 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: Isabelle: A Generic Theorem Prover

paper_content:

Foundations.- Getting started with Isabelle.- Advanced methods.- Basic use of Isabelle.- Proof management: The subgoal module.- Tactics.- Tacticals.- Theorems and forward proof.- Theories, terms and types.- Defining logics.- Syntax transformations.- Substitution tactics.- Simplification.- The classical reasoner.- Basic concepts.- First-order logic.- Zermelo-Fraenkel set theory.- Higher-order logic.- First-order sequent calculus.- Constructive Type Theory.- Syntax of Isabelle Theories.
---
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: A probabilistic extension of intuitionistic logic

paper_content:

We introduce a probabilistic extension of propositional intuitionistic logic. The logic allows making statements such as P≥sα, with the intended meaning “the probability of truthfulness of α is at least s”. We describe the corresponding class of models, which are Kripke models with a naturally arising notion of probability, and give a sound and complete infinitary axiomatic system. We prove that the logic is decidable.
---
paper_title: Reasoning about knowledge and probability

paper_content:

We provide a model for reasoning about knowledge and probability together. We allow explicit mention of probabilities in formulas, so that our language has formulas that essentially say "according to agent i, formula φ holds with probability at least α." The language is powerful enough to allow reasoning about higher-order probabilities, as well as allowing explicit comparisons of the probabilities an agent places on distinct events. We present a general framework for interpreting such formulas, and consider various properties that might hold of the interrelationship between agents' subjective probability spaces at different states. We provide a complete axiomatization for reasoning about knowledge and probability, prove a small model property, and obtain decision procedures. We then consider the effects of adding common knowledge and a probabilistic variant of common knowledge to the language.
---
paper_title: A framework for reasoning about time and reliability

paper_content:

A logic is presented for stating properties such as 'after a request for service there is at least a 98% probability that the service will be carried out within 2 s'. The logic extends the temporal logic CTL by E.A. Emerson et al. (1983) with time and probabilities. Formulas are interpreted over discrete time Markov chains. Algorithms are provided for checking that a given Markov chain satisfies a formula in the logic. An example is included to illustrate the algorithms. >
---
paper_title: A logic for reasoning about time and reliability

paper_content:

We present a logic for stating properties such as, "after a request for service there is at least a 98\045 probability that the service will be carried out within 2 seconds". The logic extends the temporal logic CTL by Emerson, Clarke and Sistla with time and probabil- ities. Formulas are interpreted over discrete time Markov chains. We give algorithms for checking that a given Markov chain satis- fies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and\003This research report is a revised and extended version of a paper that has appeared under the title "A Framework for Reasoning about Time and Reliability" in the Proceeding of the 10thIEEE Real-time Systems Symposium, Santa Monica CA, December 1989. This work was partially supported by the Swedish Board for Technical Development (STU) as part of Esprit BRA Project SPEC, and by the Swedish Telecommunication Administration.1the Markov chain. A simple example is included to illustrate the algorithms.
---
paper_title: Model Checking of Probabilistic and Nondeterministic Systems

paper_content:

The temporal logics pCTL and pCTL* have been proposed as tools for the formal specification and verification of probabilistic systems: as they can express quantitative bounds on the probability of system evolutions, they can be used to specify system properties such as reliability and performance. In this paper, we present model-checking algorithms for extensions of pCTL and pCTL* to systems in which the probabilistic behavior coexists with nondeterminism, and show that these algorithms have polynomial-time complexity in the size of the system. This provides a practical tool for reasoning on the reliability and performance of parallel systems.
---
paper_title: Quantitative analysis of probabilistic lossy channel systems

paper_content:

Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behaviour of such protocols, lossy channel systems (LCS) have been proposed. In an LCS the communication channels are modelled as FIFO buffers which are unbounded, but also unreliable in the sense that they can nondeterministically lose messages. Recently, several attempts have been made to study probabilistic lossy channel systems (PLCS) in which the probability of losing messages is taken into account and the following qualitative model checking problem is investigated: to verify whether a given property holds with probability one. Here we consider a more challenging problem, namely to calculate the probability by which a certain property is satisfied. Our main result is an algorithm for the following Quantitative model checking problem: Instance: A PLCS, its state s, a finite state @w-automaton A, and a rational @q>0. Task:Find a rational r such that the probability of the set of computations that start at s and are accepted by A is between r and r+@q. N. Bertrand, Ph. Schnoebelen, Model checking lossy channels systems is probably decidable, in: FOSSACS'03, Lecture Notes in Computer Science, vol. 2620, Springer, Berlin, 2003, pp. 120-135.] have been made to study probabilistic lossy channel systems (PLCS) in which the probability of losing messages is taken into account and the following qualitative model checking problem is investigated: to verify whether a given property holds with probability one. Here we consider a more challenging problem, namely to calculate the probability by which a certain property is satisfied. Our main result is an algorithm for the following Quantitative model checking problem: Instance: A PLCS, its state s, a finite state @w-automaton A, and a rational @q>0. Task:Find a rational r such that the probability of the set of computations that start at s and are accepted by A is between r and r+@q.
---
paper_title: It Usually Works: The Temporal Logic of Stochastic Systems

paper_content:

In this paper the branching time logic pCTL* is defined. pCTL* expresses quantitative bounds on the probabilities of correct behavior; it can be interpreted over discrete Markov processes. A bisimulation relation is defined on finite Markov processes, and shown to be sound and complete with respect to pCTL*. We extend the universe of models to generalized Markov processes in order to support notions of refinement, abstraction, and parametrization. Model checking pCTL* over generalized Markov processes is shown to be elementary by a reduction to RCF. We conclude by describing practical and theoretical avenues for further work.
---
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: Automatic Verification of Real-time Systems with Discrete Probability Distributions

paper_content:

We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, using the algorithm of [5] with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, "with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2".
---
paper_title: Model checking probabilistic timed automata with one or two clocks

paper_content:

Probabilistic timed automata are an extension of timed automata with discrete probability distributions.We consider model-checking algorithms for the subclasses of probabilistic timed automata which have one or two clocks. Firstly, we show that PCTL probabilistic model-checking problems (such as determining whether a set of target states can be reached with probability at least 0.99 regardless of how nondeterminism is resolved) are PTIME-complete for one clock probabilistic timed automata, and are EXPTIME-complete for probabilistic timed automata with two clocks. Secondly, we show that the model-checking problem for the probabilistic timed temporal logic PTCTL is EXPTIME-complete for one clock probabilistic timed automata. However, the corresponding model-checking problem for the subclass of PTCTL which does not permit both (1) punctual timing bounds, which require the occurrence of an event at an exact time point, and (2) comparisons with probability bounds other than 0 or 1, is PTIME-complete.
---
paper_title: Discrete Linear-time Probabilistic Logics: Completeness, Decidability and Complexity

paper_content:

We introduce a propositional and a first-order logic for reasoning about discrete linear time and finitely additive probability. The languages of these logics allow formulae that say 'sometime in the future, α holds with probability at least s'. We restrict our study to so-called measurable models. We provide sound and complete infinitary axiomatizations for the logics. Furthermore, in the propositional case decidability is proved by establishing a periodicity argument for ω-sequences extending the decidability proof of standard propositional temporal logic LTL. Complexity issues are examined and a worst-case complexity upper bound is given. Extensions of the presented results and open problems are described in the final part of the paper.
---
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: 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: Reasoning with Time and Chance (Extended Abstract)

paper_content:

The temporal propositional logic of linear time is generalized to an uncertain world, in which random events may occur. The formulas do not mention probabilities explicitly, i.e. the only probability appearing explicitly in formulas is probability one. This logic is claimed to be useful for stating and proving properties of probabilistic programs. It is convenient for proving those properties that do not depend on the specific distribution of probabilities used in the program's random draws. The formulas describe properties of execution sequences. The models are stochastic systems, with state transition probabilities. Three different axiomatic systems are proposed and shown complete for general models, finite models and models with bounded transition probabilities respectively. All three systems are decidable, by the results of Rabin [Ra1].
---
paper_title: On the extremely fair treatment of probabilistic algorithms

paper_content:

A proof system based on linear temporal logic for the qualitative verification of concurrent probabilistic programs is proposed. The concept of extreme fairness is introduced as an approximation to the notion of probabilistic executions. The proof system proposed is shown to be relatively complete with respect to validity over all extremely fair computations. The proof methodology is demonstrated by proving correctness of a new probabilistic algorithm for solving the mutual exclusion problem ([CLP]).
---
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: Verifying temporal properties of finite-state probabilistic programs

paper_content:

The complexity of testing whether a finite-state (sequential or concurrent) probabilistic program satisfies its specification expressed in linear temporal logic. For sequential programs an exponential-time algorithm is given and it is shown that the problem is in PSPACE; this improves the previous upper bound by two exponentials and matches the known lower bound. For concurrent programs is is shown that the problem is complete in double exponential time, improving the previous upper and lower bounds by one exponential each. These questions are also addressed for specifications described by omega -automata or formulas in extended temporal logic. >
---
paper_title: Probabilistic temporal logics for finite and bounded models

paper_content:

We present two (closely-related) propositional probabilistic temporal logics based on temporal logics of branching time as introduced by Ben-Ari, Pnueli and Manna and by Clarke and Emerson. The first logic, PTL f , is interpreted over finite models, while the second logic, PTL b , which is an extension of the first one, is interpreted over infinite models with transition probabilities bounded away from 0. The logic PTL f allows us to reason about finite-state sequential probabilistic programs, and the logic PTL b allows us to reason about (finite-state) concurrent probabilistic programs, without any explicit reference to the actual values of their state-transition probabilities. A generalization of the tableau method yields exponential-time decision procedures for our logics, and complete axiomatizations of them are given. Several meta-results, including the absence of a finite-model property for PTL b , and the connection between satisfiable formulae of PTL b and finite state concurrent probabilistic programs, are also discussed.
---
paper_title: On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties

paper_content:

In this paper, we introduce an extension of Duration Calculus called Simple Probabilistic Duration Calculus (SPDC) to express dependability requirements for real-time systems, and address the problem to decide if a probabilistic timed automaton satisfies a SPDC formula. We prove that the problem is decidable for a class of SPDC called probabilistic linear duration invariants, and provide a model checking algorithm for solving this problem.
---
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: A Probabilistic Duration Calculus

paper_content:

This paper presents a calculus that enables a designer of an embedded, real-time system to reason about and calculate whether a given requirement will hold with a sufficient high probability for given failure probabilities for components used in the design of the system. The main idea is to specify requirements and design in Duration Calculus, a real-time, interval logic, to define satisfaction probabilities for formulas in this calculus, and establish a calculus with rules that support calculation of the probability for a composite formula from probabilities of its constituents. This ensures that reasoning about probabilities is consistent with requirements and design decisions. We thus avoid introducing separate models for requirements and reliability analysis. The system model is a finite automaton with fixed transition probabilities. This defines discrete Markov processes as basis for the calulus. Keywords: duration calculus, real-time systems, probabilistic automata, satisfaction probability.
---
paper_title: Probabilistic Duration Calculus for Continuous Time

paper_content:

This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed to be written as formulas in Duration Calculus. Implementations are modelled by continuous semi-Markov processes with finite state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model.
---
paper_title: Automatic Verification of Real-time Systems with Discrete Probability Distributions

paper_content:

We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, using the algorithm of [5] with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, "with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2".
---
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: Probabilistic Neighbourhood Logic

paper_content:

This paper presents a probabilistic extension of Neighbourhood Logic (NL[14,1],). The study of such an extension is motivated by the need to supply the Probabilistic Duration Calculus (PDC,[10,4]) with a proof system. The relation between the new logic and PDC is similar to that between DC [15] and ITL [12,3]. We present a complete proof system for the new logic.
---
paper_title: Probabilistic Duration Calculus for Continuous Time

paper_content:

This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed to be written as formulas in Duration Calculus. Implementations are modelled by continuous semi-Markov processes with finite state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model.
---
paper_title: Qualitative Probability in a Modal Setting

paper_content:

Publisher Summary This chapter presents propositional calculi that are obtained by adding to modal propositional calculi a binary operator ≳ carrying the intuitive meaning of “at least as probable as.” Extending ideas because of Kripke, a semantic modeling suitable for this kind of logic is presented in the chapter. It is shown that filtration theory can be modified in such a way that completeness can be established by using well-known theorem from measurement theory. It is assumed that the reader has some familiarity with Kripke type semantics for modal logic and with filtration theory. The basic logic for PK is that P is for probability and K is for Kripke, and it is axiomatized by the following axiom system.
---
paper_title: A decidable propositional dynamic logic with explicit probabilities

paper_content:

A propositional version of Feldman and Harel's Pr DL (1982, “14th ACM Sympos. on Theory of Computing,” pp. 181–195; J. Comput. System Sci. 28 , No. 2 (1984), 193–215) is defined, and shown to be decidable in double-exponential space. The logic allows propositional-level formulas involving probabilistic programs, and contains the full (quantified) real-number theory for dealing with probabilities. The decidability proof introduces a succession of abstractions of the notion of a model, from the full generality of measure theoretical models, down to the finite schematic models , which seem to be the most basic structures relating programs and probabilities.
---
paper_title: Semantics of probabilistic programs

paper_content:

Two complementary but equivalent semantic interpretations of a high level probabilistic programming language are given. One of these interprets programs as partial measurable functions on a measurable space. The other interprets programs as continuous linear operators on a Banach space of measures. It is shown how the ordered domains of Scott and others are embedded naturally into these spaces. Two general results about probabilistic programs are proved.
---
paper_title: A decidable propositional probabilistic dynamic logic

paper_content:

A propositional version of Feldman and Harel's Pr ( DL ) is defined, and shown to be decidable. The logic allows propositional-level formulas involving probabilistic programs, and contains full real-number theory for dealing with probabilities. The decidability proof introduces model schemes, which seem to be the most basic structures relating programs and probabilities.
---
paper_title: A probabilistic PDL

paper_content:

In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk program.
---
paper_title: A Propositional Dynamic Logic with Qualitative Probabilities

paper_content:

This paper presents an ω-completeness theorem for a new propositional probabilistic logic, namely, the dynamic propositional logic of qualitative probabilities (D Q P), which has been introduced by the author as a dynamic extension of the logic of qualitative probabilities (Q P) introduced by Segerberg.
---
paper_title: A probabilistic dynamic logic

paper_content:

A logic, Pr (DL) , is presented, which enables reasoning about probabilistic programs or, alternatively, reasoning probabilistically about conventional programs. The syntax of Pr (DL) derives from Pratt's first-order dynamic logic and the semantics extends Kozen's semantics of probabilistic programs. An axiom system for Pr (DL) is presented and shown to be complete relative to an extension of first-order analysis. For discrete probabilities it is shown that first-order analysis actually suffices. Examples are presented, both of the expressive power of Pr (DL) , and of a proof in the axiom system.
---
paper_title: Probabilistic temporal logics via the modal mu-calculus

paper_content:

This paper presents a mu-calculus-based modal logic for describing properties of reactive probabilistic labeled transition systems (RPLTSs) and develops a model-checking algorithm for determining whether or not states in finite-state RPLTSs satisfy formulas in the logic. The logic is based on the distinction between (probabilistic) "systems" and (nonprobabilistic) "observations": using the modal mu-calculus, one may specify sets of observations, and the semantics of our logic then enable statements to be made about the measures of such sets at various system states. The logic may be used to encode a variety of probabilistic modal and temporal logics; in addition, the model-checking problem for it may be reduced to the calculation of solutions to systems of non-linear equations. Finally, the logic induces an equivalence on RPLTSs that coincides with accepted notions of probabilistic bisimulation in the literature.
---
paper_title: A probabilistic extension of intuitionistic logic

paper_content:

We introduce a probabilistic extension of propositional intuitionistic logic. The logic allows making statements such as P≥sα, with the intended meaning “the probability of truthfulness of α is at least s”. We describe the corresponding class of models, which are Kripke models with a naturally arising notion of probability, and give a sound and complete infinitary axiomatic system. We prove that the logic is decidable.
---
paper_title: A Logic for Reasoning about Probabilities

paper_content:

A language for reasoning about probability is considered that allows statements such as 'the probability of E/sub 1/ is less than 1/3' and 'the probability of E/sub 1/ is at least twice the probability of E/sub 2/', where E/sub 1/ and E/sub 2/ are arbitrary events. The case is treated in which all events are measurable (i.e. represent measurable sets), as well as the more general case, which is also of interest in practice, where they may not be measurable. The measurable case is essentially a formalization of (the propositional fragment of) N. Nilson's (1986) probabilistic logic, while the general (nonmeasurable) case corresponds precisely to replacing probability functions by Dempster-Shafer belief functions. In both cases, an elegant complete axiomization is provided, and it is shown that the problem of deciding satisfiability is NP-complete. >
---
paper_title: A decidable propositional dynamic logic with explicit probabilities

paper_content:

A propositional version of Feldman and Harel's Pr DL (1982, “14th ACM Sympos. on Theory of Computing,” pp. 181–195; J. Comput. System Sci. 28 , No. 2 (1984), 193–215) is defined, and shown to be decidable in double-exponential space. The logic allows propositional-level formulas involving probabilistic programs, and contains the full (quantified) real-number theory for dealing with probabilities. The decidability proof introduces a succession of abstractions of the notion of a model, from the full generality of measure theoretical models, down to the finite schematic models , which seem to be the most basic structures relating programs and probabilities.
---
paper_title: A probabilistic PDL

paper_content:

In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk program.
---
paper_title: Reasoning about knowledge and probability

paper_content:

We provide a model for reasoning about knowledge and probability together. We allow explicit mention of probabilities in formulas, so that our language has formulas that essentially say "according to agent i, formula φ holds with probability at least α." The language is powerful enough to allow reasoning about higher-order probabilities, as well as allowing explicit comparisons of the probabilities an agent places on distinct events. We present a general framework for interpreting such formulas, and consider various properties that might hold of the interrelationship between agents' subjective probability spaces at different states. We provide a complete axiomatization for reasoning about knowledge and probability, prove a small model property, and obtain decision procedures. We then consider the effects of adding common knowledge and a probabilistic variant of common knowledge to the language.
---
paper_title: Decidability and expressiveness for first-order logics of probability

paper_content:

Decidability and expressiveness issues for two first-order logics of probability are considered. In one the probability is on possible worlds, whereas in the other it is on the domain. It turns out that in both cases it takes very little to make reasoning about probability highly undecidable. It is shown that, when the probability is on the domain, if the language contains only unary predicates, then the validity problem is decidable. However, if the language contains even one binary predicate, the validity problem is Pi /sub 1//sup 2/ as hard as elementary analysis with free predicate and function symbols. With equality in the language, even with no other symbol, the validity problem is at least as hard as that for elementary analysis, Pi /sub infinity //sup 1/. Thus, the logic cannot be axiomatized in either case. When the probability is on the set of possible worlds, the validity problem is Pi /sub 1//sup 2/ complete with as little as one unary predicate in the language, even without equality. With equality, Pi /sub infinity //sup 1/ hardness with only a constant symbol is obtained. In many applications it suffices to restrict attention to domains of a bounded size; it is shown that the logics are decidable in this case. >
---

Title: Real-time and Probabilistic Temporal Logics: An Overview

Section 1: Introduction
Description 1: This section introduces the key concepts and significance of temporal logics in specifying and analyzing real-time and control systems. It summarizes different aspects such as expressiveness and complexity trade-offs, and outlines the focus areas of the paper: basic temporal framework, real-time, and probabilistic aspects of temporal logics.

Section 2: Preliminaries
Description 2: This section discusses the fundamental criteria for classifying temporal logics, such as propositional versus first-order, point-based versus interval-based, linear versus branching, discrete versus continuous, and others. It includes a historical overview of interval-based temporal logics and temporal structure properties.

Section 3: Real-Time Temporal Logics
Description 3: This section provides an overview of various well-known real-time temporal logics and their characteristics, including expressiveness, order, time metric, temporal modalities, time model, and time structure.

Section 4: Real-time Extensions of CTL
Description 4: This section details specific extensions of Computation Tree Logic (CTL) for real-time applications, including RTCTL, TCTL, and others. It covers their properties, decidability, and model-checking complexities.

Section 5: Real-Time Logic (RTL)
Description 5: This section introduces Real-Time Logic (RTL) for reasoning about events and their relations in real-time, discussing its syntactical structure, expressiveness, and the associated decision procedures' complexity.

Section 6: Real-Time Temporal Logic (RTTL)
Description 6: This section covers Real-Time Temporal Logic (RTTL), a first-order explicit clock logic, discussing its structure, interpretation over discrete and dense domains, and model-checking issues.

Section 7: Metric Temporal Logic (MTL)
Description 7: This section discusses Metric Temporal Logic (MTL), a propositional bounded-operator logic, including its expressiveness, decision problems, and model-checking complexities.

Section 8: Real-Time Interval Logic (RTIL)
Description 8: This section introduces Real-Time Interval Logic (RTIL), detailing its properties and how it formalizes specifications with a neater syntax compared to point-based logics.

Section 9: Temporal Interval Logic with Compositional Operators (TILCO)
Description 9: This section presents Temporal Interval Logic with Compositional Operators (TILCO), focusing on its expressive power for specifying real-time system behaviors.

Section 10: Probabilistic Logics
Description 10: This section provides an overview of probabilistic reasoning in formal systems with uncertainty. It reviews various probabilistic temporal logics and their distinctive features.

Section 11: The Logics PCTL and PCTL*
Description 11: This section discusses Probabilistic Computation Tree Logic (PCTL) and its extension PCTL*, detailing their syntax, semantics, and model-checking algorithms.

Section 12: The Logic PTCTL
Description 12: This section introduces Probabilistic Temporal Computational Tree Logic (PTCTL), explaining how it combines temporal and probabilistic aspects for formalizing properties in real-time systems.

Section 13: The Logic PLTL
Description 13: This section covers Probabilistic Linear Temporal Logic (PLTL), focusing on its syntax, interpretations, and applicable decision problems.

Section 14: The Logics P T L f and P T L b
Description 14: This section details two probabilistic branching time temporal logics, P T L f and P T L b, their syntax, semantics, and their use in reasoning about sequential and concurrent programs.

Section 15: The Logic PDC
Description 15: This section introduces Probabilistic Duration Calculus (PDC), discussing its properties, syntax, and the application in reasoning about probabilistic real-time systems.

Section 16: The Logic PNL
Description 16: This section discusses Probabilistic Neighbourhood Logic (PNL), its interpretation, expressive power, and proof system.

Section 17: Probabilistic Dynamic Logics
Description 17: This section reviews probabilistic dynamic logics that have been used to formalize and verify properties of probabilistic programs.

Section 18: Probabilistic Mu-Calculus
Description 18: This section introduces Generalised Probabilistic Logic (GPL), a Mu-Calculus-based modal logic, and discusses its model-checking algorithm.

Section 19: Probabilistic Instuitionistic Logics
Description 19: This section discusses propositional probabilistic intuitionistic logics, their syntax, semantics, and associated decision problems.

Section 20: Probabilistic Logics with New Types of Probability Operators
Description 20: This section covers probabilistic logics with novel probabilistic operators that allow for more complex probabilistic expressions not possible with traditional probabilistic logics.

Section 21: Probabilistic Logics for Reasoning About Knowledge and Uncertainty
Description 21: This section reviews logics that combine probabilistic reasoning with knowledge representation, summarizing key results and proof systems.

Section 22: Conclusion
Description 22: This section summarizes the key points discussed in the paper, reflecting on decidability, axiomatizability, expressiveness, and model checking of the temporal logics analyzed.