Recently we established an analog of Gabbay's separation theorem about linear temporal logic (LTL) for the extension of Moszkowski's discrete time propositional Interval Temporal Logic (ITL) by two sets of expanding modalities, namely the unary neighbourhood modalities and the binary weak inverses of ITL's chop operator. One of the many useful applications of separation in LTL is the concise proof of LTL's expressive completeness wrt the monadic first-order theory of 〈ω,<〉 it enables. In this paper we show how our separation theorem about ITL facilitates a similar proof of the expressive completeness of ITL with expanding modalities wrt the monadic first- and second-order theories of 〈Z,<〉.

In this paper, we further develop a recently introduced semantic link between temporal logics and Petri nets. We focus on two specific formalisms, Interval Temporal Logic (ITL) and Box Algebra (BA), which are closely related by their compositional approach to constructing system descriptions. The overall goal of our investigation is to translate Petri nets into behaviourally equivalent logical formulas. As a result, the analysis of system properties can be carried out using either of the two formalisms, exploiting their respective strengths and powerful tool support. The contribution of this paper is twofold. First, we extend the existing translation from BA to ITL, by removing restrictions concerning the way control flow of concurrent system is modelled, and by allowing a fully general synchronisation operator. Second, we strengthen the notion of equivalence between a Petri net and the corresponding logical formula by proving such an equivalence at the level of transition-based executions of Petri nets rather than just by looking at their labels. We also show that the complexity of the proposed translation compares favourably with the complexity of the translation from BA expressions to Petri nets.

Abstract We revisit the earliest temporal projection operator Π in discrete-time Propositional Interval Temporal Logic (PITL) and use it to formalise interleaving concurrency. The logical properties of Π as a normal modality and a way to eliminate it in both PITL and conventional point-based Linear-Time Temporal Logic (LTL), which can be viewed as a PITL subset, are examined, as are stutter-invariant formulas. Striking similarities between the expressiveness of Π and the standard LTL operator U (‘until’) are briefly illustrated. We also formalise concurrent imperative programming constructs with and without Π , and relate the two approaches. Peterson’s mutual exclusion algorithm is used to illustrate reasoning with Π about a concrete programming example. Projection with fairness and non-fairness assumptions are both discussed. This all illustrates an approach to the analysis of such concurrent interleaving finite-state systems using temporal logic formulas with projection constructs to reason about correctness properties. Unlike conventional LTL formulas about concurrency which normally largely focus on global time, properties expressed in LTL combined with Π help to reveal and analyse important differing viewpoints involving global time and the local projected time seen by each individual process. Links between Π and another standard PITL projection operator, both suitable for reasoning about different time granularities, are demonstrated by showing the two operators to be interdefinable. We briefly look at other (mostly interval-based) temporal logics with similar forms of projection, as well as some related applications and industrial standards.

We apply Interval Temporal Logic (ITL), an established temporal formalism for reasoning about time periods, to extending known facts by looking at them in reverse and then reducing reasoning about infinite time to finite time. Time reversal then helps to compositionally analyse some aspects of concurrent behaviour involving mutual exclusion.

Temporal logic has been extensively utilized in academia and industry to formally specify and verify behavioural properties of numerous kinds of hardware and software. We present a novel way to apply temporal logic to the study of a version of itself, namely, propositional linear-time temporal logic (PTL). This involves a hierarchical framework for obtaining standard results for PTL, including a small model property, decision procedures and axiomatic completeness. A large number of the steps involved are expressed in a propositional version of Interval Temporal Logic (ITL) which is referred to as PITL. It is a natural generalization of PTL and includes operators for reasoning about periods of time and sequential composition. Versions of PTL with finite time and infinite time are both considered and one benefit of the framework is the ability to systematically reduce infinitetime reasoning to finite-time reasoning. The treatment of PTL with the operator until and past time naturally reduces to that for PTL without either one. The interval-oriented methodology differs from other analyses of PTL which typically

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 /spl omega/-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 axiom system (and completeness) is extended to infinite time.

Modularity is of fundamental importance in computer science. The need for a formal theory of modularity in the design and maintenance of large systems is especially pronounced. In recent work on Interval Temporal Logic (ITL) we gave an axiom system in which proofs of sequential and parallel systems can be decomposed into proofs for the syntactic subcomponents. This provides a precise framework for describing and generalizing the insights of Francez and Pnueli (1978) and Jones (1983) for modular reasoning about concurrency using what are often called assumptions and commitments. It combines the benefits of these ideas with temporal logic. We now show that such techniques can be used to analyze temporal projection operators developed by us for describing systems with multiple time granularities. In addition, we consider how to compositionally reason in ITL about the absence of deadlock in systems running for infinite time. This demonstrates that our generalization of Jones' techniques for assumptions and commitments handles not only safety properties but also liveness ones.