Abstract
Partial orders based verifications methods are now well developed. In this framework, several suitable logics have already been defined. We focus on this paper on the logic TrPTL, as defined by Thiagarajan, for which models are the well known (infinite) Mazurkiewicz traces. We study the case where the alphabet is not connected. Our main theoretical result is that any TrPTL formula can be decomposed in an effective way as the disjunction of formulas on the connected components. Note that this result can be viewed as a direct logical counterpart of the famous Mezei's theorem on recognizable sets in a direct product of free monoids.
Finally, we show that our result can also be of practical interest. Precisely, we exhibit families of formulas for which the use of our decomposition procedure decreases the complexity of the decision procedure of satisfiability.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Preview
Unable to display preview. Download preview PDF.
References
J. Berstel. Transductions and context-free languages. Teubner Studienbücher, 1979.
V. Diekert. Combinatorics on Traces. Number 454 in LNCS. Springer, 1990.
V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.
W. Ebinger and A. Muscholl. Logical definability on infinite traces. In A. Lingas, R. Karlsson, and S. Carlsson, editors, Proc. of the 20th ICALP, Lund (Sweden) 1993, number 700 in LNCS, pages 335–346. Springer, 1993.
P. Gastin and A. Petit. Asynchronous automata for infinite traces. In W. Kuich, editor, Proc. of the 19th ICALP, Vienna (Austria) 1992, number 623 in LNCS, pages 583–594. Springer, 1992.
P. Gastin, A. Petit, and W. Zielonka. An extension of Kleene's and Ochmański's theorems to infinite traces. Theoret. Comp. Sci., 125:167–204, 1994. A preliminary version was presented at ICALP'91, LNCS 510 (1991).
P. Godefroid and P. Wolper. A partial approach to model checking. Inform. and Comp., 110:305–326, 1994.
S. Katz and D. Peled. Interleaving set temporal logic. Theoret. Comp. Sci., 75:21–43, 1992.
K. Lodaya, R. Ramajunam, and P.S. Thiagarajan. Temporal logics for communicating sequential agents:I. Int. J. of Found. of Comp. Sci., 3(2):117–159, 1992.
A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.
M. Mukund and P.S. Thiagarajan. A logical characterization of well branching event structures. Theoret. Comp. Sci., 96:35–72, 1992.
M. Mukund and P.S. Thiagarajan. Linear time temporal logics over Mazurkiewicz traces. In Proc. of the 21th MFCS, 1996, number 1113 in LNCS, pages 62–92. Springer, 1996.
W. Penczek. A temporal logic for event structures. Fundamenta Informaticae, XI:297–326, 1988.
W. Penczek and R. Kuiper. Traces and logic. In V. Diekert and G. Rozenberg, editors, The book of Traces, pages 307–381, 1995.
A. Pnueli. The temporal logics of programs. In Proc. of the 18th IEEE FOCS, 1977, pages 46–57, 1977.
P.S. Thiagarajan. A trace based extension of linear time temporal logic. In Proc. of the 9th LICS, 1994, pages 438–447, 1994.
W. Thomas. On logical definability of trace languages. In V. Diekert, editor, Proc. an ASMICS workshop, Kochel am See 1989, Report TUM-19002, Technical University of Munich, pages 172–182, 1989.
W. Thomas. Automata on infinite objects. In J. v. Leeuwen, editor, Handbook of Theoretical Computer Science, pages 133–191. Elsevier Science Publishers, 1990.
P.S. Thiagarajan and l. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. In Proc. of LICS'97 (to appear), 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, R., Petit, A. (1997). Decomposition of TrPTL formulas. In: Prívara, I., Ružička, P. (eds) Mathematical Foundations of Computer Science 1997. MFCS 1997. Lecture Notes in Computer Science, vol 1295. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0029985
Download citation
DOI: https://doi.org/10.1007/BFb0029985
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63437-9
Online ISBN: 978-3-540-69547-9
eBook Packages: Springer Book Archive