The power of the future perfect in program logics

DOI10.1016/S0019-9958(85)80025-5zbMath0582.68010MaRDI QIDQ3704887

Colin Stirling, Matthew C. B. Hennessy

Publication date: 1985

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

zbMATH Keywords

bisimulationtense logictemporal logicbehavioural equivalencetransition systemsHennessy-Milner logicinfinite computationrelativised past tense operator

Mathematics Subject Classification ID

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

Related Items (15)

Compositionality of Hennessy-Milner logic by structural operational semantics ⋮ Efficient timed model checking for discrete-time systems ⋮ Bisimulation maps in presheaf categories ⋮ Representation of decision making processes in an ecological evaluation system ⋮ An algebraic characterization of observational equivalence ⋮ Characterizing finite Kripke structures in propositional temporal logic ⋮ SOS formats and meta-theory: 20 years after ⋮ Bisimulation, games, and logic ⋮ Interpreting one concurrent calculus in another ⋮ Translations between modal logics of reactive systems ⋮ \(R\)-generability, and definability in branching time logics ⋮ Event Identifier Logic ⋮ Algebraic characterizations of trace and decorated trace equivalences over tree-like structures ⋮ Modal logics for communicating systems ⋮ A Logic for True Concurrency

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