- Abstract:
-
Monadic second order logic (MSOL) provides a general framework for expressing properties of reactive systems as modelled by trees. Monadic path logic (MPL) is obtained by restricting second order quantification to paths reflecting computation sequences. In this paper we show that the expressive power of MPL over trees coincides with the usual branching time logic CTL* embellished with a simple form of counting. As a corollary, we derive an earlier result that CTL* coincides with the bisimulation-invariant properties of MPL. In order to prove the main result, we first prove a new Composition Theorem for trees.
- Copyright:
- 2001 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0041,
- author = {
Alexander Rabinovich
and Faron Moller
},
- title = {Counting on CTL* : On the Expressive Power of Monadic Path Logic},
- year = 2001,
- month = {Jun},
- }
|
