scientific article; zbMATH DE number 176726

MaRDI QIDQ4036555zbMATH OpenFDO

Authors

Publication date 18 May 1993

zbMATH Keywords

program semanticslivenessbranching time logicbranching time semanticssilent actionsinfinite computation trees modulo bisimulationsafety preordersimulation testingtree- automata

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• A lattice-theoretic characterization of safety and liveness
• An abstract interpretation-based model for safety semantics
• Safety, liveness and fairness in temporal logic
• Recognizing safety and liveness
• Modalities for model checking: Branching time logic strikes back

Cited in

(23)

• Requirements, specifications, and minimal refinement
• Minimal refinements of specifications in modal and temporal logics
• Minimal refinements of specifications in modal and temporal logics
• Compositional verification of sequential programs with procedures
• An abstract interpretation-based model for safety semantics
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Equivalence checking 40 years after: a review of bisimulation tools
• “On the fly” verification of behavioural equivalences and preorders
• Property preserving abstractions for the verification of concurrent systems
• Towards the hierarchical verification of reactive systems
• Sharp congruences adequate with temporal logics combining weak and strong modalities
• Translating FSP into LOTOS and networks of automata
• Selective mu-calculus and formula-based equivalence of transition systems
• Coupled similarity: the first 32 years
• Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous
• Compositional verification of asynchronous concurrent systems using CADP
• Refined Interfaces for Compositional Verification
• Inference of -languages from prefixes.
• On hierarchically developing reactive systems
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Cartesian difference categories
• Reduced models for efficient CCS verification
• Reducing behavioural to structural properties of programs with procedures

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 Q4036555)