Search

In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages , i.e. languages whose structure is immediately "visible" in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of operator precedence languages. This "historical" language family has been recently proved to enjoy fundamental algebraic and logic properties that make it suitable for model checking applications yet breaking the barrier of visible-structure languages (in fact the original motivation of its inventor Floyd was just to support efficient parsing , i.e. building the "hidden syntax tree" of language sentences). We prove that our logic is at least as expressive as analogous logics defined for visible pushdown languages yet covering a much more powerful family; we design a procedure that, given a formula in our logic builds an automaton recognizing the sentences satisfying the formula, whose size is at most exponential in the length of the formula. Our results cover both finite and infinite string languages. [ABSTRACT FROM AUTHOR]

Theorem proving is one of the most widely used approaches to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a sound and complete proof system for Propositional Projection Temporal Logic (PPTL) with indexed expressions, which is a unified temporal logic that subsumes the well used Linear Temporal Logic (LTL). First, the syntax, semantics and logic laws of PPTL that allows indexed expressions are introduced, and the representation of LTL constructs by PPTL formulas is illustrated. Then, the proof system for the logic is presented which consists of axioms and inference rules for the derivation of both basic constructs and indexed expressions. To show the capability of the proof system, several examples of formal proofs are provided. Finally, the soundness and completeness of the proof system are demonstrated. [ABSTRACT FROM AUTHOR]

Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECT L + were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CT L ⋆ , often considered as 'the full branching-time logic' overcomes these restrictions on expressing fairness. However, CT L ⋆ is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for CT L ⋆ , while one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more 'natural' being more friendly for human understanding. These two considerations lead to the following problem - are there logics that have richer expressiveness than ECT L + , allowing the formulation of a new range of fairness constraints with 'until' operator, yet 'simpler' than CT L ⋆ , and for which a one-pass tableau can be developed? Here we give a positive answer to this question, introducing a sub-logic of CT L ⋆ called ECT L # , its tree-style one-pass tableau, and an algorithm for obtaining a systematic tableau, for any given admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi. Our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECT L # , and of a dual sequent calculi. [ABSTRACT FROM AUTHOR]

Halpern and Shoham modal logic of time intervals (HS in short) is an elegant and highly influential propositional interval-based modal logic. Its sub-propositional fragments, that is fragments obtained by restricting use of propositional connectives, and their hybrid extensions with nominals and satisfaction operators have been recently studied and successfully applied in real-world use cases. Detailed investigation of their decidability and computational complexity has been conducted, however, there has been significantly less research on their expressive power. In this paper we make a step towards filling this gap. In particular, we (1) compare classes of frames definable in full HS and in its hybrid extension, and (2) determine in which sub-propositional HS -fragments we can express the difference operator, nominals, and satisfaction operators. The obtained results enable us to classify HS , its sub-propositional fragments, and their hybrid extensions according to their expressive power. [ABSTRACT FROM AUTHOR]

In Temporal Logic (TL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions , are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed since their equivalent concise syntax formulas can be found. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax by means of fixed-point approach. Firstly, we present two kinds of formulas, namely ⋁ i ∈ N 0 ◯ i Q and ⋁ i ∈ N 0 Q i , and prove they are indeed well-formed by proving they are equivalent to formulas ◇ Q and Q ⁎ respectively. Further, we generalize ⋁ i ∈ N 0 ◯ i Q to ⋁ i ∈ N 0 P (i) ∧ ◯ i Q and explore the least and greatest fixed-points of an abstract equation X ≡ Q ∨ P ∧ ◯ X. Based on these, some well-formed special instances of ⋁ i ∈ N 0 P (i) ∧ ◯ i Q are obtained. Besides, with the index set expression technique, we equivalently represent ' U ' (strong until) and ' W ' (weak until) constructs of propositional Linear Temporal Logic (LTL) within Propositional Projection Temporal Logic (PPTL). [ABSTRACT FROM AUTHOR]

To specify properties of open systems with interval based temporal logics, Alternating Projection Temporal Logic (APTL) is proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL). Further, examples are given to show how properties of open systems can be specified by APTL formulas. Moreover, to establish the automata based model theory for the new proposed logic, Generalized alternating Büchi automata over Concurrent Game structures (GBCGs) are defined, and a transformation from APTL formulas to GBCGs is presented. In addition, a decision procedure for checking the satisfiability of APTL formulas, and a model checking approach for APTL with Concurrent Game Structures (CGSs) being models are presented. [ABSTRACT FROM AUTHOR]

Some extensions of ω -regular languages have been proposed in the literature to express asymptotic properties of ω -words which are not captured by ω -regular languages. They include ωB -regular languages, that extend ω -regular languages with boundedness, ωS -regular languages, that enrich ω -regular ones with strong unboundedness, ωBS -regular languages, that combine ωB - and ωS -regular ones, and ωT -regular languages, that include meaningful languages which are not ωBS -regular. Formal definitions of extended ω -regular languages have been given in terms of both suitable classes of automata and extended ω -regular expressions, while satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics by providing an explicit encoding of expressions into formulas. [ABSTRACT FROM AUTHOR]

Abstract: We define the spatio-temporal logic MTLA as an extension of Lamport''s Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics. [Copyright &y& Elsevier]

Abstract: The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp). The ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc LTL formula. This paper presents new positive decidability results for timed ccp as well as for LTL. In particular, we shall prove that the following problems are decidable: (1) the sp equivalence for the so-called locally-independent ntcc fragment; unlike other fragments for which similar results have been published, this fragment can specify infinite-state systems, (2) verification for locally-independent processes and negation-free first-order formulae of the ntcc LTL, (3) implication for such formulae, (4) Satisfiability for a first-order fragment of Manna and Pnueli''s LTL. The purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency. [Copyright &y& Elsevier]

This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MetricIntervalTL formulae into EventClockTL formulae, the two logics being equally expressive. Our proof is structured to yield axiomatizations also for interesting fragments of these logics, such as the linear temporal logic of the real numbers (TLR). [Copyright &y& Elsevier]