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

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