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 | Symposium on Logic in Computer Science - Paris, France Duration: 1 Jan 1994 → … |
Conference
Conference | Symposium on Logic in Computer Science |
---|---|
City | Paris, France |
Period | 01/01/1994 → … |