Branching versus linear logics yet again

DOI10.1007/BF01888216zbMath0697.68022OpenAlexW2018583412MaRDI QIDQ911747

José Carmo, Amílcar Sernadas

Publication date: 1990

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01888216

zbMATH Keywords

completenessaxiomatisationstemporal logicssafety and livenessframe change operatorsinformation systems specification and verificationlinear and branching modelsstate and path formulas

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Information storage and retrieval of data (68P20)

Related Items

Temporal Logic and Fair Discrete Systems ⋮ Branching vs. Linear Time: Semantical Perspective ⋮ A Branching Time Logical System for Open Distributed Systems Development ⋮ Branching time logics with multiagent temporal accessibility relations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maintaining knowledge about temporal intervals
• The temporal logic of branching time
• Transformation of dynamic integrity constraints into transaction specifications
• The INFOLOG linear tense propositional logic of events and transactions
• Modeling concurrency with partial orders
• Specification and verification of database dynamics
• Temporal aspects of logical procedure definition
• Petri nets, event structures and domains. I
• Axiomatising the logic of computer programming
• Process logic: Expressiveness, decidability, completeness
• First-order dynamic logic
• Propositional dynamic logic of regular programs
• Alternative semantics for temporal logics
• A complete deductive-system for since-until branching-time logic
• Tense systems with discrete moments of time. I
• Reasoning with time and chance
• “Sometimes” and “not never” revisited
• The unreal future
• Proving Liveness Properties of Concurrent Programs
• Guarded commands, nondeterminacy and formal derivation of programs
• An axiomatic basis for computer programming
• Indeterminist time and truth‐value gaps¹