Abstract:
Linear temporal logic (LTL) has become a well established tool for specifying the dynamic behavior of reactive systems with an interleaving semantics and the automatatheoretic approach has proven to be a very useful mechanism for performing automatic verification in this setting. Especially alternating automata turned out to be a powerful tool in constructing efficient yet simple to understand decision procedures and directly yield on-the-fly model checking procedures. While this technique extends elegantly to richer domains where the underlying computations are modeled as (Mazurkiewicz) traces, it does so only for eventand location-based temporal logics. In this thesis, we exhibit a decision procedure for LTL over Mazurkiewicz traces which generalizes the classical automata-theoretic approach to a linear temporal logic interpreted no longer over sequences but restricted labeled partial orders. Specifically, we construct a (linear) alternating Buchi automaton accepting the set of linearizations of those traces satisfying the formula at hand. The salient point of our technique is to apply a notion of independencerewriting to formulas of the logic. Furthermore, we show that the class of linear and trace-consistent alternating Buchi automata corresponds exactly to LTL formulas over Mazurkiewicz traces, lifting a similar result from Loding and Thomas formulated in the framework of LTL over words. Additionally, a linear temporal logic with a different flavor is introduced as Foata linear temporal logic (LTLf). It is designed for specifying properties of synchronized systems that comprise clocked hardware circuits or Petri nets supplied with a maximal step semantics. Distributed synchronous transition systems (DSTSs) are introduced as formal models of these systems and are equipped with a Foata configuration graph-based semantics, which provides a link between these systems and the framework of Mazurkiewicz traces. To simplify the task of defining DSTSs, we introduce a simple calculus in the spirit of CCS. We give optimal decision procedures for satisfiability of LTLf formulas as well as for model checking, both based on alternating Buchi automata. The model checking procedure further employs an optimization which is similar to a technique known as partial order reduction.Keywords:
Büchi automaton
TRACE (psycholinguistics)
Computation tree logic
Interleaving
Cite
Formalism (music)
Punctuality
Cite
Citations (41)
Cite
Citations (2)
Bisimulation
Transition system
Cite
Citations (3)
In this paper we describe a technique for monitoring and checking temporal logic assertions augmented with real-time and time-series constraints, or Metric Temporal Logic Series (MTLS). The method is based on Remote Execution and Monitoring (REM) of temporal logic assertions. We describe the syntax and semantics of MTLS and a monitoring technique based on alternating finite automata that is efficient for a large set of frequently used formulae and is also an on-line technique. We investigate the run-time data-structure size for several interesting assertions taken from the Kansas State specification patterns.
Computation tree logic
Cite
Citations (8)
Model checking is an algorithmic technique for checking if a concurrent system satisfies a given property expressed in an appropriate temporal logic. LTLC(linear temporal logic with clocks) is a continuous-time temporal logic proposed for the specification of real-time systems. It is a real-time extension of the temporal logic LTL. In this paper, the model checking problem for LTLC is discrssed and a reduction from LTLC model checking to LTL model checking is presented. This reduction will enable us to use the existing LTL model checking tools for LTLC model checking. Owing to the fact that LTLC can express both the properties and the implementations of real-time systems, the LTLC model checking procedures can be used for both the property verification and the refinement verification for real-time systems with finite locations.
Abstraction model checking
Computation tree logic
Cite
Citations (1)
TRACE (psycholinguistics)
Satisfiability
Completeness (order theory)
Boolean satisfiability problem
Cite
Citations (16)
Computation tree logic
Assertion
Büchi automaton
On the fly
Cite
Citations (702)
Branching (polymer chemistry)
Cite
Citations (0)
Transitive closure
Computation tree logic
Transition system
Logic model
First-order logic
Cite
Citations (27)
Formalism (music)
Computation tree logic
Abstraction model checking
Cite
Citations (2)