Verifying Temporal Properties of Systems

Research output: Book/ReportBook

Abstract

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 languageEnglish
PublisherBirkhäuser
ISBN (Print)9780817636258
Publication statusPublished - 1992

Publication series

NameProgress in Theoretical Computer Science Series
PublisherBirkhäuser

Fingerprint

Dive into the research topics of 'Verifying Temporal Properties of Systems'. Together they form a unique fingerprint.

Cite this