Abstract
We continue our study of the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In a previous paper (CONCUR 2003), we investigated the class of local and MSO definable temporal logics that capture all known temporal logics and we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed). In this paper, we concentrate on the uniform satisfiability problem: we consider the dependence alphabet (i.e., the architecture of the distributed system) as part of the input. We prove lower and upper bounds for the uniform satisfiability problem that depend on the number of monadic quantifier alternations present in the chosen MSO-modalities.
Work partly supported by the DAAD-PROCOPE project Temporal and Quantitative Analysis of Distributed Systems.
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. IEEE Computer Society Press, Los Alamitos (1995)
Diekert, V., Gastin, P.: Local temporal logic is expressively complete for cograph dependence alphabets. Information and Computation 195, 30–52 (2004)
Diekert, V., Gastin, P.: Pure future local temporal logics are expressively complete for Mazurkiewicz traces. In: Farach-Colton, M. (ed.) LATIN 2004. LNCS, vol. 2976, pp. 232–241. Springer, Heidelberg (2004)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1991)
Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic. Oxford University Press, Oxford (1994)
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)
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)
Schwentick, T., Bartelmann, K.: Local normal forms for first-order logic with applications to games and automata. Discrete Mathematics and Computer Science 3, 109–124 (1999)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gastin, P., Kuske, D. (2005). Uniform Satisfiability Problem for Local Temporal Logics over Mazurkiewicz Traces. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_40
Download citation
DOI: https://doi.org/10.1007/11539452_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)