Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, E-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
Identifiers
URN: urn:nbn:se:kth:diva-62956DOI: 10.1016/j.entcs.2011.10.018Scopus ID: 2-s2.0-80155198604OAI: oai:DiVA.org:kth-62956DiVA: diva2:481417
Funder
ICT - The Next Generation
Note
4th workshop on Logical Aspect of Multi-Agent systems. QC 20120124Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2017-12-08Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Dam, Mads

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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 48 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf