An epistemic predicate CTL* for finite control pi-processes
2011 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 278, no 1, 229-243 p.Article in journal (Refereed) Published
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*.
Place, publisher, year, edition, pages
2011. Vol. 278, no 1, 229-243 p.
epistemic temporal logic, pi-calculus, model checking
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-62956DOI: 10.1016/j.entcs.2011.10.018ScopusID: 2-s2.0-80155198604OAI: oai:DiVA.org:kth-62956DiVA: diva2:481417
FunderICT - The Next Generation
4th workshop on Logical Aspect of Multi-Agent systems. QC 201201242012-01-202012-01-202012-06-13Bibliographically approved