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
Model Checking Mobile Processes (Full version)
RISE, Swedish ICT, SICS.
1994 (English)Report (Other academic)
Abstract [en]

We introduce a temporal logic for the polyadic pi-calculus based on fixed point extensions of Hennessy-Milner logic. Features are added to account for parametrisation, generation, and passing of names, including the use, following Milner, of dependent sum and product to account for (unlocalised) input and output, and explicit parametrisation on names using lambda-abstraction and application. The latter provides a single name binding mechanism supporting all parametrisation needed. A proof system and decision procedure is developed based on Stirling and Walker's approach to model checking the modal mu-calculus using constants. One difficulty, for both conceptual and efficiency-based reasons, is to avoid the explicit use of the omega-rule for parametrised processes. A key idea, following Hennessy and Lin's approach to deciding bisimulation for certain types of value-passing processes, is the relativisation of correctness assertions to conditions on names. Based on this idea a proof system and decision procedure is obtained for arbitrary pi-calculus processes with finite control, pi-calculus correlates of CCS finite-state processes, avoiding the use of parallel composition in recursively defined processes.

Place, publisher, year, edition, pages
Swedish Institute of Computer Science , 1994, 1.
Series
SICS Research Report, ISSN 0283-3638 ; R94:01
Keyword [en]
Temporal Logic, Process Algebra, Mobile Processes, Model Checking
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-21375OAI: oai:DiVA.org:ri-21375DiVA: diva2:1041411
Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2017-08-25Bibliographically approved

Open Access in DiVA

fulltext(3594 kB)0 downloads
File information
File name FULLTEXT01.pdfFile size 3594 kBChecksum SHA-512
04178360f52c7c60d9076aea214fdf49cbb3e8de9fd304c83f6e3b204fd9b2910b16e45e5052d86e245dd1f3e4c0d31616dbe3ebe25e5f2324845cf53ab89934
Type fulltextMimetype application/pdf

By organisation
SICS
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

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
v. 2.28.0