Abstract
This paper presents the notion of Present-Future form (PF form) for linear time -calculus (TL) formulas consisting of the present and future parts: the present part is the conjunction of atomic propositions or their negations while the future part is a closed TL formula under the next operator. We show every closed TL formula can be rewritten into its corresponding PF form. Finally, based on PF form, the idea of constructing a graph that describing models of a TL formula is discussed. © 2014 Springer International Publishing Switzerland.
Author supplied keywords
Cite
CITATION STYLE
Liu, Y., Duan, Z., Tian, C., & Liu, B. (2014). Present-future form of linear time μ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8332 LNCS, pp. 76–85). Springer Verlag. https://doi.org/10.1007/978-3-319-04915-1_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
