Title :
A compositional proof system for the modal μ-calculus
Author :
Andersen, Henrik Reif ; Stirling, Colin ; Winskel, Glynn
Author_Institution :
Dept. of Comput. Sci., Tech. Univ. Denmark, Lyngby, Denmark
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
Keywords :
formal logic; theorem proving; compositional proof system; compositional reasoning; finite-state processes; local model checking; modal μ-calculus; process algebra; Algebra; Calculus; Computer science; Councils; Logic functions; Power system modeling; Turning;
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
DOI :
10.1109/LICS.1994.316076
