Abstract
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes
Original language | English |
---|---|
Title of host publication | Proceedings of the symposium of Logic in Computer Science |
Publisher | IEEE |
Publication date | 1994 |
Pages | 144-153 |
ISBN (Print) | 08-18-66310-3 |
DOIs | |
Publication status | Published - 1994 |
Event | Ninth Annual Symposium on Logic in Computer Science - Paris, France Duration: 4 Jul 1994 → 7 Jul 1994 |
Conference
Conference | Ninth Annual Symposium on Logic in Computer Science |
---|---|
Country/Territory | France |
City | Paris |
Period | 04/07/1994 → 07/07/1994 |