Anzeige
Erschienen in:
1990 | ReviewPaper | Buchkapitel
Proving properties of elementary net systems with a special-purpose theorem prover
verfasst von : Heikki Tuominen
Erschienen in: Automatic Verification Methods for Finite State Systems
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Elementary net systems, basic net-theoretic models of distributed systems, as well as their properties are represented by formulas of deterministic propositional dynamic logic. A semantic tableaux based theorem prover is used to verify the properties, i.e. to find out whether they are entailed by the representations of the systems. The theorem prover implements a simplified tableaux decision procedure, the simplifications are due to the special nature of the set of formulas representing an elementary net system.