Abstract
To specify properties of open systems with interval based temporal logics, alternating interval based temporal logics are proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL) and Propositional Interval Temporal Logic (PITL). Further, examples are given to show how properties of open systems can be specified by APTL and AITL formulas. Moreover, to establish the automata based model theory for the new proposed logics, 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) models are presented. © 2010 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Tian, C., & Duan, Z. (2010). Alternating interval based temporal logics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6447 LNCS, pp. 694–709). https://doi.org/10.1007/978-3-642-16901-4_45
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
