Abstract
Recently, we proved that satisfiability for \(\mathsf {ECTL}^*\) with constraints over \(\mathbb {Z}\) is decidable using a new technique based on weak monadic second-order logic with the bounding quantifier (\(\mathsf {WMSO\!+\!B}\)). Here we apply this approach to concrete domains that are tree-like. We show that satisfiability of \(\mathsf {ECTL}^*\) with constraints is decidable over (i) semi-linear orders, (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching order trees of height h for each fixed \(h\in \mathbb {N}\). In contrast, we introduce Ehrenfeucht-Fraïssé-games for \(\mathsf {WMSO\!+\!B}\) (weak \(\mathsf {MSO}\) with the bounding quantifier) and use them to show that our approach cannot deal with the class of order trees. Missing proofs and details can be found in the long version [6].
This work is supported by the DFG Research Training Group 1763 (QuantLA) and the DFG research project LO-748-2 (GELO).
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
Notes
- 1.
A structure \(\mathcal {U}\) is universal for a class \(\varGamma \) if there is a homomorphic embedding of every structure from \(\varGamma \) into \(\mathcal {U}\) and \(\mathcal {U}\) belongs to \(\varGamma \).
- 2.
For a presentation of the general case we refer the reader to [5] .
- 3.
We call \((A,<,\mathrel {\bot })\) a graph to emphasize that here the binary relation symbols \(<\) and \(\mathrel {\bot }\) can have arbitrary interpretations, whence we see them as two kinds of edges in an arbitrary graph.
- 4.
For the ease of presentation we assume that \(\mathcal {A}\) and \(\mathcal {B}\) are infinite structures.
References
Bojańczyk, M., Toruńczyk, S.: Weak MSO+U over infinite trees. In: Proceedings STACS 2012, vol. 14, pp. 648–660. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)
Bozzelli, L., Gascon, R.: Branching-time temporal logic extended with qualitative presburger constraints. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 197–211. Springer, Heidelberg (2006)
Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. Theor. Comput. Sci. 523, 1–36 (2014)
Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of CTL\(^{*}\) with constraints. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 455–469. Springer, Heidelberg (2013)
Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of ECTL\({}^*\) with constraints. submitted for publication. http://www.eti.uni-siegen.de/ti/veroeffentlichungen/ectl-with-constraints.pdf
Carapelle, C., Kartzow, A., Lohrey, M., Feng, S.: Satisfiability of \({\sf ECTL} ^{*}\) with tree constraints. http://arXiv.org/abs/1412.2905
Demri, S., Deters,M.: Temporal logics on strings with prefix relation. Research Report LSV-14-13, ENS Cachan. http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2014-13.pdf
Demri, S., Gascon, R.: Verification of qualitative Z constraints. Theor. Comput. Sci. 409(1), 24–40 (2008)
Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Perspectives in Mathematical Logic, 1st edn. Springer, Heidelberg (1995)
Gascon, R.: An automata-based approach for CTL\(^{*}\) with constraints. Electron. Notes Theor. Comput. Sci. 239, 193–211 (2009)
Thomas, W.: Computation tree logic and regular omega-languages. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 690–713. Springer, Heidelberg (1989)
Vardi, M.Y., Wolper, P.: Yet another process logic. In: Clarke, E., Kozen, D. (eds.) Logics of Programs. LNCS, vol. 164, pp. 501–512. Springer, Heidelberg (1984)
Wolk, E.S.: The comparability graph of a tree. Proc. Am. Math. Soc. 13(5), 789–795 (1962)
Wolk, E.S.: A note on “the comparability graph of a tree”. Proc. Am. Math. Soc. 16(1), 17–20 (1965)
Acknowledgement
We thank Manfred Droste for fruitful discussions on universal structures and semi-linear orders and the anonymous referees.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Carapelle, C., Feng, S., Kartzow, A., Lohrey, M. (2015). Satisfiability of ECTL* with Tree Constraints. In: Beklemishev, L., Musatov, D. (eds) Computer Science -- Theory and Applications. CSR 2015. Lecture Notes in Computer Science(), vol 9139. Springer, Cham. https://doi.org/10.1007/978-3-319-20297-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-20297-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-20296-9
Online ISBN: 978-3-319-20297-6
eBook Packages: Computer ScienceComputer Science (R0)