Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces

• Autorzy: Gastin P. , Kuske D.
• Języki publikacji: EN

Abstrakty

EN

We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.

Słowa kluczowe

EN

temporal logic; Mazurkiewicz traces

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 80, nr 1-3
• Strony: 169--197
• Opis fizyczny: bibliogr. 20 poz.

Twórcy

autor

Gastin P.

autor

Kuske D.

• LSV, ENS Cachan&CNRS, France,

Bibliografia

• [1] R. Alur, R. Peled, andW. Penczek. Model checking of causality properties. In LICS 95, pages 90-100. IEEE Computer Society Press, 1995.
• [2] V. Diekert and P. Gastin. LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences, 64:396-418, 2002. A preliminary version appeared at ICALP'00, Lecture Notes in Comp. Science vol. 1853, pages 211-222, Springer.
• [3] V. Diekert and P. Gastin. Local temporal logic is expressively complete for cograph dependence alphabets. Information and Computation, 195:30-52, 2004. A preliminary version appeared at LPAR'01, Lecture Notes in Artificial Intelligence vol. 2250, pages 55-69, Springer.
• [4] V. Diekert and P. Gastin. Pure future local temporal logics are expressively complete forMazurkiewicz traces. Information and Computation, 204:1597-1619, 2006. A preliminary version appeared at LATIN'04, Lecture Notes in Comp. Science vol. 2976, pages 232-241, Springer.
• [5] V. Diekert and G. Rozenberg. The Book of Traces. World Scientific Publ. Co., 1995.
• [6] P. Gastin and D. Kuske. Satisfiability andmodel checking forMSO-definable temporal logics are in PSPACE. In R. Amadio and D. Lugiez, editors, CONCUR'03, Lecture Notes in Comp. Science vol. 2761, pages 222-236. Springer, 2003.
• [7] P. Gastin and D. Kuske. Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. In L. de Alfaro, editor, CONCUR'05, Lecture Notes in Comp. Science vol. 3653, pages 533-547. Springer, 2005.
• [8] P. Gastin and M. Mukund. An elementary expressively complete temporal logic for Mazurkiewicz traces. In ICALP'02, Lecture Notes in Comp. Science vol. 2380, pages 938-949. Springer, 2002.
• [9] S. Katz and D. Peled. Interleaving set temporal logic. Theoretical Comp. Science, 75:21-43, 1991.
• [10] O. Kupferman and M. Vardi. Weak alternating automata are not that weak. ACM Transaction on Computational Logic, 2(3):408-429, 2001.
• [11] A. Mazurkiewicz. Concurrent program schemes and their interpretation. Technical report, DAIMI Report PB-78, Aarhus University, 1977.
• [12] A. Mazurkiewicz. Trace theory. InW. Brauer and others, editor, Petri Nets, Applications and Relationship to other Models of Concurrency, Lecture Notes in Comp. Science vol. 255, pages 279-324. Springer, 1987.
• [13] S. Miyano and T. Hayashi. Alternating finite automata on !-words. Theoretical Comp. Science, 32:321-330, 1984.
• [14] W. Penczek. A concurrent branching time temporal logic. In E. Börger, H. Kleine Büning, and M.M. Richter, editors, 3rd Workshop on Computer Science Logic, Lecture Notes in Comp. Science vol. 440, pages 337-354. Springer, 1990.
• [15] W. Penczek. On undecidability of temporal logics on trace systems. Information Processing Letters, 43:147-153, 1992.
• [16] D. Perrin and J.-E. Pin. Infinite Words. Pure and Applied Mathematics vol. 141. Elsevier, 2004.
• [17] S. Safra. On the complexity of omega-automata. In FOCS'88, pages 319-327. IEEE Computer Society Press, 1988.
• [18] P.S. Thiagarajan. A trace based extension of linear time temporal logic. In LICS'94, pages 438-447. IEEE Computer Society Press, 1994.
• [19] P.S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. Information and Computation, 179:230-249, 2002. A preliminary version appeared at LICS'97, pages 183-194, IEEE Computer Society Press.
• [20] I. Walukiewicz. Difficult configurations - on the complexity of LTrL. In ICALP'98, Lecture Notes in Comp. Science vol. 1443, pages 140-151. Springer, 1998.