Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

LICS

1994

IEEE

1994

IEEE

The modal mu-calculus is an expressive logic that can be used to specify safety and liveness properties of concurrent systems represented as labeled transition systems (LTSs). We show that Model Checking in the Modal Mu-Calculus (MCMMC) -- the problem of checking whether an LTS is a model of a formula of the propositional modal mu-calculus -is P-complete even for a very restrictive version of the problem involving the alternationfree fragment. In particular, MCMMC is P-complete even if the formula is fixed and alternation-free, and the LTS is deterministic, acyclic, and has fan-in and fan-out bounded by 2. The reduction used is from a restricted version of the circuit value problem (Does a circuit output a 1 on inputs x1, . . ., xn?) known as Synchronous Alternating Monotone Fanout 2 Circuit Value Problem. Our P-completeness result is tight in the sense that placing any further non-trivial restrictions on either the formula or the LTS results in membership in NC for MCMMC. Specifical...

Related Content

Added |
09 Aug 2010 |

Updated |
09 Aug 2010 |

Type |
Conference |

Year |
1994 |

Where |
LICS |

Authors |
Shipei Zhang, Oleg Sokolsky, Scott A. Smolka |

Comments (0)