Academic
Publications
Simple on-the-fly automatic verification of linear temporal logic

Simple on-the-fly automatic verification of linear temporal logic,Rob Gerth,Doron Peled,Moshe Y. Vardi,Pierre Wolper

Simple on-the-fly automatic verification of linear temporal logic   (Citations: 418)
BibTex | RIS | RefWorks Download
We present a tableau-based algorithm for obtaining an automaton from a temporal logic formula. The algorithm is geared towards being used in model checking in an "on-the-fly" fas hion, that is the automaton can be constructed simultaneously with, and guided by, the generation of the model. In particular, it is possible to detect that a property does not hold by only const ructing part of the model and of the automaton. The algorithm can also be used to check the validity of a temporal logic assertion. Although the general problem is PSPACE-complete, experiments show that our algorithm performs quite well on the temporal formulas typically encount ered in verification. While basing linear-time temporal logic model-checking upon a transformation to automata is not new, the details of how to do this efficiently, and in "on-the-fly" f ashion have never been given.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...An online monitoring algorithm adapted from the on-the-fly verification of linear temporal logic [10] is also presented...

    Guoquan Wuet al. Runtime Monitoring of Data-centric Temporal Properties for Web Service...

    • ...Theorem 1: [20] A LTL formula f is satisfied iff there exists a path of states in the f-automata (finite with no successor at the last state or infinite)starting from the starting prestate and such that any occurrence of Future and Until modal operator in a state of the path fulfills its corresponding promise operand later (in the future) in the path...
    • ...[20], [33]) use nested deep-first-search of fair loop or simple deep first search of fair SCC...
    • ...The unwinding follows the Algorithm 3. Those unwound formulas are valid formulas and of the form pres( ) ) disjpres( ) where disjpres( ) is the classical unwinding of formulas at the state of tableau [20], [33]...

    Francois Hantryet al. Detection of Conflicting Compliance Rules

    • ...The fact that logics such as LTL (linear-time temporal logic) or CTL (computation tree logic) can be efficiently translated into corresponding automata [10, 11, 26, 28 ]h as facilitated their integration into main verification tools...

    Kevin D. Joneset al. Analog property checkers: a DDR2 case study

    • ...Efficient translation implementations have been developed in [15], [16]...

    Stephen L. Smithet al. Optimal Path Planning under Temporal Logic Constraints

    • ...LTL translation algorithm was described in [26]...
    • ...Does size matter? The focus of almost all LTL translation papers, starting with [26], has been on minimizing automata size...

    Kristin Y. Rozieret al. LTL satisfiability checking

Sort by: