A provably correct compiler for efficient model checking of mobile processes

Ping Yang; Yifei Dong; C. R. Ramakrishnan; Scott A. Smolka

doi:10.1007/978-3-540-30557-6_10

A provably correct compiler for efficient model checking of mobile processes

Ping Yang
, Yifei Dong
, C. R. Ramakrishnan
, Scott A. Smolka

Computer Science

Stony Brook University
University of Oklahoma

Research output: Contribution to journal › Conference article › peer-review

3 Scopus citations

Abstract

We present an optimizing compiler for the π-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the π-calculus handles names by representing π-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a π-calculus process P, our compiler for MMC produces an extremely compact representation of P's symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry.

Original language	English
Pages (from-to)	113-127
Number of pages	15
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3350
DOIs	https://doi.org/10.1007/978-3-540-30557-6_10
State	Published - 2005
Event	7th International Symposium on Practical Aspects of Declarative Languages, PADL 2005 - Long Beach, CA, United States Duration: Jan 10 2005 → Jan 11 2005

Access to Document

10.1007/978-3-540-30557-6_10

Cite this

@article{e3cf9ecb8fcb4c0bbd98a49ce902315d,

title = "A provably correct compiler for efficient model checking of mobile processes",

abstract = "We present an optimizing compiler for the π-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the π-calculus handles names by representing π-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a π-calculus process P, our compiler for MMC produces an extremely compact representation of P's symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry.",

author = "Ping Yang and Yifei Dong and Ramakrishnan, \{C. R.\} and Smolka, \{Scott A.\}",

year = "2005",

doi = "10.1007/978-3-540-30557-6\_10",

language = "English",

volume = "3350",

pages = "113--127",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

note = "7th International Symposium on Practical Aspects of Declarative Languages, PADL 2005 ; Conference date: 10-01-2005 Through 11-01-2005",

}

A provably correct compiler for efficient model checking of mobile processes. / Yang, Ping; Dong, Yifei; Ramakrishnan, C. R. et al.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 3350, 2005, p. 113-127.

Research output: Contribution to journal › Conference article › peer-review

TY - JOUR

T1 - A provably correct compiler for efficient model checking of mobile processes

AU - Yang, Ping

AU - Dong, Yifei

AU - Ramakrishnan, C. R.

AU - Smolka, Scott A.

PY - 2005

Y1 - 2005

N2 - We present an optimizing compiler for the π-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the π-calculus handles names by representing π-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a π-calculus process P, our compiler for MMC produces an extremely compact representation of P's symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry.

AB - We present an optimizing compiler for the π-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the π-calculus handles names by representing π-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a π-calculus process P, our compiler for MMC produces an extremely compact representation of P's symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry.

UR - https://www.scopus.com/pages/publications/23944515356

U2 - 10.1007/978-3-540-30557-6_10

DO - 10.1007/978-3-540-30557-6_10

M3 - Conference article

AN - SCOPUS:23944515356

SN - 0302-9743

VL - 3350

SP - 113

EP - 127

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 7th International Symposium on Practical Aspects of Declarative Languages, PADL 2005

Y2 - 10 January 2005 through 11 January 2005

ER -

A provably correct compiler for efficient model checking of mobile processes

Abstract

Access to Document

Other files and links

Fingerprint

Cite this