Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Counting on CTL* : On the Expressive Power of Monadic Path Logic
Authors: Alexander Rabinovich ; Faron Moller
Date:Jun 2001
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.
2001 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Alexander Rabinovich and Faron Moller },
title = {Counting on CTL* : On the Expressive Power of Monadic Path Logic},
year = 2001,
month = {Jun},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh