Abstract
The paper settles a long standing problem for Mazurkiewicz traces: the pure future local temporal logic defined with the basic modalities exists-next and until is expressively complete. The analogous result with a global interpretation was solved some years ago by Thiagarajan and Walukiewicz (1997) and in its final form without any reference to past tense constants by Diekert and Gastin (2000). Each, the (previously known) global or the (new) local result generalizes Kamp’s Theorem for words, because for sequences local and global viewpoints coincide. But traces are labelled partial orders and then the difference between an interpretation globally over cuts (configurations) or locally at points (events) is significant. For global temporal logics the satisfiability problem is non-elementary (Walukiewicz 1998), whereas for local temporal logics both the satisfiability problem and the model checking problem are solvable in Pspace (Gastin and Kuske 2003) as in the case of words. This makes local temporal logics much more attractive.
Work done while the second author stayed in Stuttgart within the MERCATOR program of the German Research Foundation DFG. Partial support of ACI Sécurité Informatique 2003-22 (VERSYDIS) is gratefully acknowledged.
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
Adsul, B., Sohoni, M.: Complete and tractable local linear time temporal logics over traces. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 926–937. Springer, Heidelberg (2002)
Alur, R., Peled, D., Penczek, W.: Model-checking of causality properties. In: Proc. of LICS 1995, pp. 90–100 (1995)
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.: LTL is expressively complete for Mazurkiewicz traces. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 211–222. Springer, Heidelberg (2000)
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.: LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences 64, 396–418 (2002)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Ebinger, W.: Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart (1994)
Ebinger, W., Muscholl, A.: Logical definability on infinite traces. Theoretical Computer Science 154, 67–84 (1996)
Gastin, P., Kuske, D.: Satisfiability and model checking for MSO-definable temporal logics are in PSPACE. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 222–236. Springer, Heidelberg (2003)
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)
Gastin, P., Mukund, M., Narayan Kumar, K.: Local LTL with past constants is expressively complete for Mazurkiewicz traces. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 429–438. Springer, Heidelberg (2003)
Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, California (1968)
Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus (1977)
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)
Niebert, P.: A ν-calculus with local views for sequential agents. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 563–573. Springer, Heidelberg (1995)
Penczek, W.: Temporal logics for trace systems: On automated verification. International Journal of Foundations of Computer Science 4, 31–67 (1993)
Ramanujam, R.: Locally linear time temporal logic. In: Proc. of LICS 1996, pp. 118–128 (1996)
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., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. In: Proc. of LICS 1997, pp. 183–194 (1997)
Walukiewicz, A.: Difficult configurations – on the complexity of LTrL. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 140–151. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Diekert, V., Gastin, P. (2004). Pure Future Local Temporal Logics Are Expressively Complete for Mazurkiewicz Traces. In: Farach-Colton, M. (eds) LATIN 2004: Theoretical Informatics. LATIN 2004. Lecture Notes in Computer Science, vol 2976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24698-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-24698-5_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21258-4
Online ISBN: 978-3-540-24698-5
eBook Packages: Springer Book Archive