Anzeige
Erschienen in:
2018 | OriginalPaper | Buchkapitel
Symbolic Model Checking in Non-Boolean Domains
verfasst von : Rupak Majumdar, Jean-François Raskin
Erschienen in: Handbook of Model Checking
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
We consider symbolic model checking as a general procedure to compute fixed points on general lattices. We show that this view provides a unified approach for formal reasoning about systems that is applicable to many different classes of systems and properties. Our unified view is based on the notion of region algebras together with appropriate generalizations of the modal μ$\mu$-calculus. We show applications of our general approach to problems in infinite-state verification, reactive synthesis, and the analysis of probabilistic systems.