Rules for trace consistent reasoning

DOI10.1007/3-540-63875-X_43MaRDI QIDQ4370348zbMATH OpenFDO

Authors Ramaswamy Ramanujam

Publication date 15 July 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63875-X_43

zbMATH Keywords

axiomatizationcommon actionsfinite-state agentsmodel of distributed systemspartial-order methodspropositional temporal logictrace consistent formulastransition system

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The paper deals with linear time propositional temporal logic (PTL), and focuses on trace consistent formulas, i.e., those which do not distinguish between two interleavings of the same (partially-ordered) run in the underlying transition system. This notion was previously studied from the `model-checking viewpoint', while here the author applies an axiomatic approach. He chooses a structurally straightforward subset of PTL and a simple model of distributed systems -- finite-state agents which are synchronized via common actions. Then he elaborates a complete axiomatization system for the valid formulas, which is a nontrivial task despite of the simplicity of the chosen setting. Besides giving the mentioned technical result, the paper adds some insight how to separate the properties which can be analyzed locally from those which have to be analyzed globally in a distributed system. For the entire collection see [Zbl 0878.00079].

Recommendations

• Distributed versions of linear time temporal logic: A trace perspective
• scientific article; zbMATH DE number 2086683
• scientific article; zbMATH DE number 845931
• scientific article; zbMATH DE number 512851

Cited in

(2)

• Tracking reasons with extensions of relevant logics
• Trace consistency and inevitability

This page was built for publication: Rules for trace consistent reasoning

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