Abstract
Temporal logics over Mazurkiewicz traces have been extensively studied over the past fifteen years. In order to be usable for the verification of concurrent systems they need to have reasonable complexity for the satisfiability and the model checking problems. Whenever a new temporal logic was introduced, a new proof (usually non trivial) was needed to establish the complexity of these problems. In this paper, we introduce a unified framework to define local temporal logics over traces. We prove that the satisfiability problem and the model checking problem for asynchronous Kripke structures for local temporal logics over traces are decidable in PSPACE. This subsumes and sometimes improves all complexity results previously obtained on local temporal logics for traces.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Peled, R., Penczek, W.: Model checking of causality properties. In: LICS 1995, pp. 90–100. IEEE Computer Society Press, Los Alamitos (1995)
Büchi, J.R.: On a decision method in restricted second order arithmetics. In: Nagel, E., et al. (eds.) Proc. Intern. Congress on Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press, Stanford (1960)
Diekert, V.: A pure future local temporal logic beyond cograph-monoids. In: Ito, M. (ed.) Proc. of the RIMS Symposium on Algebraic Systems, Formal Languages and Conventional and Unconventional Computation Theory, Kyoto, Japan (2002)
Diekert, V., Gastin, P.: Local temporal logic is expressively complete for cograph dependence alphabets. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 55–69. Springer, Heidelberg (2001)
Diekert, V., Gastin, P.: Local temporal logic is expressively complete for cograph dependence alphabets. Tech. Rep. LIAFA, Universit´e Paris 7, France (2003), http://www.liafa.jussieu.fr/~gastin/Articles/diegas03.html
Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific Publ. Co., Singapore (1995)
Gastin, P., Mukund, M.: An elementary expressively complete temporal logic for Mazurkiewicz traces. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 938–949. Springer, Heidelberg (2002)
Kamp, H.W.: Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, USA (1968)
Kupferman, O., Piterman, N., Vardi, M.Y.: Extended temporal logic revisited. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 519–535. Springer, Heidelberg (2001)
Mukund, M., Sohoni, M.: Keeping trace of the latest gossip: bounded timestamps suffice. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 388–399. Springer, Heidelberg (1993)
Mukund, M., Thiagarajan, P.S.: Linear time temporal logics over Mazurkiewicz traces. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 62–92. Springer, Heidelberg (1996)
Rabinovich, A., Maoz, S.: An infinite hierarchy of temporal logics over branching time. Information and Computation 171(2), 306–332 (2001)
Thiagarajan, P.S.: A trace based extension of linear time temporal logic. In: Proc. of LICS 1994, pp. 438–447. IEEE Computer Society Press, Los Alamitos (1994)
Thiagarajan, P.S.: A trace consistent subset of PTL. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 438–452. Springer, Heidelberg (1995)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 133–191. Elsevier Science Publ. B.V., Amsterdam (1990)
Vardi, M.Y., Wolper, P.: Reasonning about infinite computations. Information and Computation 115, 1–37 (1994)
Wolper, P.: Temporal logic can be more expressive. Inf. and Control 56, 72–99 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gastin, P., Kuske, D. (2003). Satisfiability and Model Checking for MSO-Definable Temporal Logics Are in PSPACE. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-45187-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40753-9
Online ISBN: 978-3-540-45187-7
eBook Packages: Springer Book Archive