The modal mu-calculus is a powerful logic with which to express properties of concurrent systems. There are algorithms which allow one to check whether a finite system satisfies a formula of this logic; but many interesting systems are infinite, or at least potentially infinite. In this paper we present an approach to verifying infinite systems. The method is a tableau style proof system, using the modal mu-calculus as the logic. We also describe a software tool to assist humans in using the method.
Original language | English |
---|
Publisher | Birkhäuser |
---|
ISBN (Print) | 9780817636258 |
---|
Publication status | Published - 1992 |
---|
Name | Progress in Theoretical Computer Science Series |
---|
Publisher | Birkhäuser |
---|