Abstract
In this paper, we study linear time \(\mu \)-calculus interpreted over finite traces, namely \(\nu \)TL\(_f\). We define Present Future form (PF form) for \(\nu \)TL\(_f\) formulas and prove that every closed \(\nu \)TL\(_f\) formula can be converted into this form. PF form decomposes a formula into two parts: what to be satisfied at the current state and what to be satisfied at the next one. Based on PF form, we provide an algorithm for constructing Present Future form Graph (PFG) that can be employed to depict models of a formula. In addition, a decision procedure for checking satisfiability of \(\nu \)TL\(_f\) formulas based on PFG is proposed.
This research is supported by the NSFC Grant Nos. 61133001, 61322202, 91418201, and 61420106004.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bacchus, F., Kabanza, F.: Planning for temporally extended goals. Ann. Math. Artif. Intell. 22(1–2), 5–27 (1998)
Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 62–74. Springer, Heidelberg (1989)
Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL 1986, pp. 173–183. ACM Press, New York (1986)
Bradfield, J.C., Esparza, J., Mader, A.: An effective tableau system for the linear time \(\mu \)-calculus. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 98–109. Springer, Heidelberg (1996)
Bruse, F., Friedmann, O., Lange, M.: On guarded transformation in the modal \(\mu \)-calculus. Logic J. IGPL 23(2), 194–216 (2015)
Calvanese, D., De Giacomo, G., Vardi, M.Y.: Reasoning about actions and planning in LTL action theories. In: Fensel, D., Giunchiglia, F., McGuinness, D.L., Williams, M.A. (eds.) KR 2002, pp. 593–602. Morgan Kaufmann, San Francisco (2002)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \(\mu \)-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273–284. Springer, Heidelberg (2006)
De Giacomo, G., Vardi, M.Y.: Automata-theoretic approach to planning for temporally extended goals. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol. 1809, pp. 226–238. Springer, Heidelberg (2000)
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI 2013, pp. 854–860. AAAI Press, Palo Alto (2013)
Duan, Z.: An extended interval temporal logic and a framing technique for temporal logic programming. Ph.D. thesis, University of Newcastle upon Tyne (1996)
Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2006)
Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theor. Comput. Sci. 554, 169–190 (2014)
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)
Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)
Kaivola, R.: A simple decision method for the linear time mu-calculus. In: Desel, J. (ed.) Proceedings of the International Workshop on Structures in Concurrency Theory, pp. 190–204. Springer, London (1995)
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983)
Liu, Y., Duan, Z., Tian, C.: A decision procedure for a fragment of linear time mu-calculus. In: Kambhampati, S. (ed.) IJCAI 2016. AAAI Press, Palo Alto (2016)
Patrizi, F., Lipoveztky, N., De Giacomo, G., Geffner, H.: Computing infinite plans for LTL goals using a classical planner. In: Walsh, T. (ed.) IJCAI 2011, pp. 2003–2008. AAAI Press, Palo Alto (2011)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE Press, New York (1977)
Stirling, C., Walker, D.: CCS, liveness, and local model checking in the linear time mu-calculus. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 166–178. Springer, Heidelberg (1990)
Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 465–472. Springer, Heidelberg (1984)
Torres, J., Baier, J.A.: Polynomial-time reformulations of LTL temporally extended goals into final-state goals. In: Yang, Q., Wooldridge, M. (eds.) IJCAI 2015, pp. 1696–1703. AAAI Press, Palo Alto (2015)
Vardi, M.Y.: A temporal fixpoint calculus. In: Ferrante, J., Mager, P. (eds.) POPL 1988, pp. 250–259. ACM Press, New York (1988)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Liu, Y., Duan, Z., Tian, C., Cui, B. (2016). Satisfiability of Linear Time Mu-Calculus on Finite Traces. In: Dinh, T., Thai, M. (eds) Computing and Combinatorics . COCOON 2016. Lecture Notes in Computer Science(), vol 9797. Springer, Cham. https://doi.org/10.1007/978-3-319-42634-1_49
Download citation
DOI: https://doi.org/10.1007/978-3-319-42634-1_49
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42633-4
Online ISBN: 978-3-319-42634-1
eBook Packages: Computer ScienceComputer Science (R0)