Change search
ReferencesLink to record
Permanent link

Direct link
An epistemic predicate CTL* for finite control pi-processes
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2011 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 278, no 1, 229-243 p.Article in journal (Refereed) Published
Abstract [en]

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.
Keyword [en]
epistemic temporal logic, pi-calculus, model checking
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-62956DOI: 10.1016/j.entcs.2011.10.018ScopusID: 2-s2.0-80155198604OAI: diva2:481417
ICT - The Next Generation
4th workshop on Logical Aspect of Multi-Agent systems. QC 20120124Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2012-06-13Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Dam, Mads
By organisation
Theoretical Computer Science, TCS
In the same journal
Electronical Notes in Theoretical Computer Science
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 35 hits
ReferencesLink to record
Permanent link

Direct link