scientific article; zbMATH DE number 52748

MaRDI QIDQ4003036zbMATH OpenFDO

Authors Julian Bradfield

Publication date 18 September 1992

zbMATH Keywords

complexity of mu-formulae on netsconcurrent systemsfixed point operatorsmodal logicmodel-checkingPetri netspropositional modal mu-calculustableau methodverification of infinite systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Temporal property verification as a program analysis task
• Verification of temporal properties
• Early verification of computer systems temporal properties
• Verifying abstractions of timed systems
• Verifying quantitative temporal properties of procedural programs
• Verifying temporal properties in real models
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 1696448
• Temporal proof methodologies for timed transition systems

Cited in

(23)

• Verification of reactive systems. Formal methods and algorithms.
• On hierarchically developing reactive systems
• Bounded model checking of infinite state systems
• Parameterised Boolean equation systems
• Model checking discounted temporal properties
• Verification on infinite structures.
• Suitability of mCRL2 for concurrent-system design: a 2 2 Switch case study
• Complementary Criteria for Testing Temporal Logic Properties
• scientific article; zbMATH DE number 139824 (Why is no real title available?)
• scientific article; zbMATH DE number 177500 (Why is no real title available?)
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• Local model checking for context-free processes
• Fixpoint alternation: arithmetic, transition systems, and the binary tree
• A Note on Negative Tagging for Least Fixed-Point Formulae
• Instantiation for Parameterised Boolean Equation Systems
• Decidability of model checking with the temporal logic EF
• Towards the hierarchical verification of reactive systems
• Free -lattices
• Reachability analysis of pushdown automata: Application to model-checking
• Modal and temporal logics for processes
• Proving liveness of fair transition systems
• Verification of reactive systems via instantiation of parameterised Boolean equation systems
• Abstract interpretation based verification of temporal properties for BioAmbients

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4003036)