An Epistemic Predicate CTL* for Finite Control π-Processes
| Autor: | Dimitar P. Guelev, Mads Dam |
|---|---|
| Rok vydání: | 2011 |
| Předmět: |
Model checking
Computation tree logic General Computer Science pi-calculus Predicate (mathematical logic) model checking Theoretical Computer Science Undecidable problem Epistemology Decidability epistemic temporal logic CTL TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Modal Linear temporal logic TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Computer Science::Formal Languages and Automata Theory Computer Science(all) Mathematics |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 278:229-243 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2011.10.018 |
| Popis: | We examine model checking of finite control π-calculus processes against specifications in epistemic predicate CTL*. In contrast to branching time settings such as CTL or the modal μ-calculus, the general problem, even for LTL, is undecidable, essentially because a process can use the environment as unbounded storage. To circumvent this problem attention is restricted to closed processes for which internal communication along a given set of known channels is observable. This allows to model processes operating in a suitably memory-bounded environment. We propose an epistemic predicate full CTL* with perfect recall which is interpreted on the computation trees defined by such finite control π-calculus processes. We demonstrate the decidability of model-checking by a reduction to the decidability of validity in quantified full propositional CTL*. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect