On First-Order Fragments for Mazurkiewicz Traces

• Autorzy: Diekert V. , Horsch M. , Kufleitner M.
• Języki publikacji: EN

Abstrakty

EN

Mazurkiewicz traces form a model for concurrency. Temporal logic and first-order logic are important tools in order to deal with the abstract behavior of such systems. Since typical properties can be described by rather simple logical formulas one is interested in logical fragments. One focus of this paper is unary temporal logic and first-order logic in two variables. Over words, this corresponds to the variety of finite monoids called DA. However, over Mazurkiewicz traces it is crucial whether traces are given as dependence graphs or as partial orders (over words these notions coincide). The main technical contribution is a generalization of important characterizations of DA from words to dependence graphs, whereas the use of partial orders leads to strictly larger classes. As a consequence we can decide whether a first-order formula over dependence graphs is equivalent to a first-order formula in two variables. The corresponding result for partial orders is not known. This difference between dependence graphs and partial orders also affects the complexity of the satisfiability problems for the fragments under consideration: for first-order formulas in two variables we prove an NEXPTIME upper bound, whereas the corresponding problem for partial orders leads to EXPSPACE. Furthermore, we give several separation results for the alternation hierarchy for first-order logic. It turns out that even for those levels at which one can express the partial order relation in terms of dependence graphs, the fragments over partial orders have more expressive power.

Słowa kluczowe

EN

Mazurkiewicz traces; temporal logic; first-order logic; Ehrenfeucht-Fraissé games

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

Twórcy

autor

Diekert V.

autor

Horsch M.

autor

Kufleitner M.

• Institut füFormale methoden der Informatik, FMI Universität Stuttgart, Universitätsstrasse 38 70569 Stuttgart, Germany,

Bibliografia

• [1] Cartier, P., Foata, D.: Problèmes combinatoires de commutation et réarrangements, Lecture Notes in Mathematics, 85, Springer, 1969. Electronic reedition available at: http://www-irma.u-strasbg.fr/~foata/paper/ProbComb.pdf
• [2] Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces, Journal of Computer and System Sciences, 64, 2002, 396-418.
• [3] Diekert, V., Gastin, P.: Pure future local temporal logics are expressively complete for Mazurkiewicz traces, Information and Computation, 204, 2006, 1597-1619, Conference version in LATIN 2004, LNCS 2976, 170-182, 2004.
• [4] Diekert, V., Rozenberg, G., Eds.: The Book of Traces, World Scientific, Singapore, 1995.
• [5] Eilenberg, S.: Automata, Languages, and Machines, vol. B, Academic Press, New York and London, 1976.
• [6] Emerson, E. A.: Temporal and Modal Logic, in: Handbook of Theoretical Computer Science (J. Van Leeuwen, Ed.), vol. B, chapter 16, Elsevier Science Publisher B. V., 1990, 995-1072.
• [7] Etessami, K., Vardi, M. Y., Wilke, Th.: First-order logic with two variables and unary temporal logic, Information and Computation, 2002, 279-295, Conference version: LICS'97.
• [8] Etessami, K., Wilke, Th.: An until hierarchy for temporal logic, Logic in Computer Science, 1996.
• [9] Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, Clarendon Press, Oxford, 1994.
• [10] Gastin, P., Kuske, D.: Satisfiability and model checking for MSO-definable temporal logics are in PSPACE, Proc. of the 14th Int. Conf. on Concurrency Theory (CONCUR'03) (R. M. Amadio, D. Lugiez, Eds.), LNCS 2761, Springer,Marseille, France, August 2003.
• [11] Gastin, P., Kuske, D.: Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces, this volume of Fundamenta Informaticae, 2007.
• [12] Gastin, P.,Mukund,M.: An elementary expressively complete temporal logic forMazurkiewicz traces, Proc. 29th Int. Colloquium on Automata, Languages and Programming (ICALP'2002) (P. Widmayer et al., eds.), LNCS 2380, Springer, 2002.
• [13] Immerman, N., Kozen, D.: Definability with bounded number of bound variables, Logic in Computer Science, 1987.
• [14] Kufleitner,M.: Logical Fragments for Mazurkiewicz Traces: Expressive Power and Algebraic Characterizations, Dissertation, Institut für Formale Methoden der Informatik, Universit¨at Stuttgart, 2006.
• [15] Kufleitner, M.: Polynomials, fragments of temporal logic and the variety DA over traces, Theoretical Computer Science, 376, 2007, 89-100. Conference version in DLT 2006, LNCS 4036, 37-48, 2006.
• [16] Mazurkiewicz, A.: Concurrent program schemes and their interpretations, DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.
• [17] Pin, J.-é., Weil, P.: Polynominal closure and unambiguous product, Theory Comput. Syst., 30(4), 1997, 383-422.
• [18] Sistla, A. P., Clarke, E.: The complexity of propositional linear time logic, Journal of the Association for Computing Machinery, 32, 1985, 733-749.
• [19] Tesson, P., Thérien, D.: Diamonds are forever: The variety DA, Semigroups, Algorithms, Automata and Languages, Coimbra (Portugal) 2001 (G. M. dos Gomes Moreira da Cunha, P. V. A. da Silva, J.-E. Pin, Eds.), World Scientific, 2002.
• [20] Thérien, D., Wilke, Th.: Over words, two variables are as powerful as one quantifier alternation, STOC, 1998.
• [21] Thiagarajan, P. S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces, Proc. 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), Warsaw (Poland), 1997.
• [22] Thomas, W.: An application of the Ehrenfeucht-Fra¨ıssé game in formal language theory, Mém. Soc. Math. de France, série 2, 16, 1984, 11-21.
• [23] Weis, P., Immerman, N.: Structure theorem and strict alternation hierarchy for FO2 on words, Proc. 16th EACSL Annual Conference on Computer Science and Logic (CSL'07), Lausanne (Switzerland) (J. Duparc and Th. Henzinger, Eds.), LNCS 4646, 2007.