Abstract
Various logical languages are compared regarding their expressive power with respect to models consisting of finitely bounded branching infinite trees. The basic multimodal logic with backward- and forward necessity operators is equivalent to restricted first order logic; by adding the binary temporal operators ”since” and ”until” we get the expressive power of first order logic on trees. Hence (restricted) propositional quantifiers in temporal logic correspond to (restricted) set quantifiers in predicate logic. Adding the CTL path modality ”E” to temporal logic gives the expressive power of path logic. Tree grammar operators give a logic as expressive as weak second order logic, whereas adding fixed point quantifiers (in the so-called propositional μ-calculus) results in a logic expressivly equivalent to monadic second order logic on trees.
This work was partly done when the author was on leave at Carnegie-Mellon-University, Pittsburgh, PA; it was supported by DFG grant Schl 310/1-1
Preview
Unable to display preview. Download preview PDF.
References
A. Arnold, D. Niwinsky: Fixed point characterization of weak monadic second order logic of trees; technical report 91-06, Laboratoire Bordelais de Recherche en Informatique, Université de Bordeaux I; (1991).
E.M. Clarke, E.A. Emerson, A.P. Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications; in: Proc. 10th ACM POPL, pp.117–126; Austin, TX (1983). reappeared in: ACM Trans. Prog. Lang. & Syst. 8.2, pp.244–263; (1986).
R. Cleaveland: Tableau-Based Model Checking in the Propositional Mu-Calculus; in: Acta Informatica 27, pp.725–747; (1990).
E.A. Emerson, J.Y. Halpern: “Sometimes” and “Not Never” Revisited: On Branching versus Linear Time (preliminary report); in: Proc. 10th ACM POPL, pp.127–140; Austin, TX (1983). reappeared in: Journal of the ACM 33.1, pp.151–178; (1986).
E.A. Emerson, C.-L. Lei: Efficient Model Checking in Fragments of the Propositional Mu-Calculus; in: Proc. IEEE Symp. on Logic in Comp. Sci., pp.267–278; Cambridge, MA (1986).
E.A. Emerson, C.S. Jutla: Tree Automata, Mu-Calculus and Determinacy, in: Proc. 32nd IEEE Symp. on Found. of Comp. Sci., pp.368–377; (1991).
T. Hafer, W. Thomas: Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree; in: T. Ottmann (ed.): ICALP 1987, LNCS 267; (1988). Short version of T. Hafer: On the Expressive Completeness of CTL *; Bericht Nr. 123, Schriften zur Informatik, RWTH Aachen; (1986).
U. Heuter: Zur Klassifizierung regulärer Baumsprachen; Dissertation, RWTH Aachen; (1989).
D. Kozen: Results on the Propositional μ-Calculus; in: Proc. 9th ICALP, LNCS 140, pp.348–359; (1982).
D. Kozen, R. Parikii: A Decision Procedure for the Propositional μ-Calculus; in: Proc. Logics of Programs, LNCS 164, pp.313–325; (1983).
D. Muller, A. Saoudi, P. Schupp: Alternating Automata Give a Simple Explanation of Why Most Temporal and Dynamic Logics Are Decidable in Exponential Time; in: Proc. 3rd IEEE Symp. on Logic in Comp. Sci., pp.422–427; (1988).
D. Niwinsky: Fixed Points vs. Infinite Generation; in: Proc. 3rd IEEE Symp. on Logic in Comp. Sci., pp.402–409; (1988).
D. Park: Concurrency an Automata on Infinite Sequences; in: Proc. 5th GI Conf. on Theor. Comp. Sci., LNCS 104, pp.167–183; (1981).
M.O. Rabin: Decidability of Second-Order Theories and Automata on Infinite Trees; in: Trans. AMS 141, pp.1–35; (1969).
M.O. Rabin: Weakly Definable Relations and Special Automata; in: Y. Bar-Hillel (ed.): Mathematical Logic and Foundations of Set Theory, pp.1–23; North-Holland, Amsterdam (1970).
B.-H. Schlingloff: Zur temporalen Logik von Bäumen; Report TUM-I9012, Institut für Informatik der Technischen Universität München; (1990).
B.-H. Schlingloff: Expressive Completeness of Temporal Logic of Trees; To appear in: Journal of Applied Non-Classical Logics 2.2; Hermes, Paris (1992).
R. Streett, E.A. Emerson: An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus; in: Information and Computation 81, pp.249–264; (1989).
M. Takahashi: The Greatest Fixed-Points and Ratinal Omega-Tree Languages; in: Theoretical Computer Science 44, pp.259–274; (1986).
P. Wolper: Temporal Logic Can Be More Expressive; in: Information and Control 56, pp.72–99; (1983).
P. Wolper, M.Y. Vardi, A.P. Sistla: Reasoning About Infinite Computation Paths; in: Proc. 24th IEEE Symp. on Found. of Comp. Sci., pp.185–194; (1983).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schlingloff, BH. (1992). On the expressive power of modal logics on trees. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023896
Download citation
DOI: https://doi.org/10.1007/BFb0023896
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive