The power of the future perfect in program logics

DOI10.1016/S0019-9958(85)80025-5MaRDI QIDQ3704887zbMATH OpenFDO

Authors Matthew Hennessy, Colin Stirling

Publication date 1985

Published in Information and Control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0019-9958(85)80025-5

zbMATH Keywords

behavioural equivalencebisimulationHennessy-Milner logicinfinite computationrelativised past tense operatortemporal logictense logictransition systems

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Theory of operating systems (68N25) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Cited in

(18)

• Characterizing finite Kripke structures in propositional temporal logic
• R-generability, and definability in branching time logics
• Representation of decision making processes in an ecological evaluation system
• An algebraic characterization of observational equivalence
• Linear future semantics and its implementation
• Bisimulation maps in presheaf categories
• Compositionality of Hennessy-Milner logic by structural operational semantics
• Efficient timed model checking for discrete-time systems
• scientific article; zbMATH DE number 6297875 (Why is no real title available?)
• A logic for true concurrency
• Event identifier logic
• Modal logics for communicating systems
• Algebraic characterizations of trace and decorated trace equivalences over tree-like structures
• Bisimulation, games, and logic
• Translations between modal logics of reactive systems
• Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities
• SOS formats and meta-theory: 20 years after
• Interpreting one concurrent calculus in another

This page was built for publication: The power of the future perfect in program logics

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