Back to Search
Start Over
A practical decision procedure for Propositional Projection Temporal Logic with infinite models.
- Source :
-
Theoretical Computer Science . Oct2014, Vol. 554, p169-190. 22p. - Publication Year :
- 2014
-
Abstract
- This paper presents a practical decision procedure for Propositional Projection Temporal Logic with infinite models. First, a set Prop l of labels l i , 0 ⩽ i ⩽ n ∈ N 0 , is used to mark nodes of an LNFG of a formula, and a node with l i is treated as an accepting state as in an automaton. Further, the generalized Büchi accepting condition for automata is employed to identify a path (resulting a word) in an LNFG as a model of the formula. In addition, the implementation details of the decision procedure and relevant algorithms including pre-processing, LNFG, circle finding algorithms are presented; as a matter of fact, all algorithms are implemented by C++ programs. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 03043975
- Volume :
- 554
- Database :
- Academic Search Index
- Journal :
- Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- 98575665
- Full Text :
- https://doi.org/10.1016/j.tcs.2014.02.011