Unifying hyper and epistemic temporal logics

DOI10.1007/978-3-662-46678-0_11MaRDI QIDQ2949438zbMATH OpenOpenAlexFDO

Authors Laura Bozzelli, Bastien Maubert, Sophie Pinchinat

Publication date 1 October 2015

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

Full work available at URL https://arxiv.org/abs/1409.2711

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logics of knowledge and belief (including belief change) (03B42) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Abstract: In the literature, two powerful temporal logic formalisms have been proposed for expressing information flow security requirements, that in general, go beyond regular properties. One is classic, based on the knowledge modalities of epistemic logic. The other one, the so called hyper logic, is more recent and subsumes many proposals from the literature; it is based on explicit and simultaneous quantification over multiple paths. In an attempt to better understand how these logics compare with each other, we consider the logic KCTL* (the extension of CTL* with knowledge modalities and synchronous perfect recall semantics) and HyperCTL*. We first establish that KCTL* and HyperCTL* are expressively incomparable. Second, we introduce and study a natural linear past extension of HyperCTL* to unify KCTL* and HyperCTL*; indeed, we show that KCTL* can be easily translated in linear time into the proposed logic. Moreover, we show that the model-checking problem for this novel logic is decidable, and we provide its exact computational complexity in terms of a new measure of path quantifiers' alternation. For this, we settle open complexity issues for unrestricted quantified propositional temporal logic.

Recommendations

• Temporal hyperproperties
• Model checking algorithms for hyperproperties (invited paper)
• A temporal logic for asynchronous hyperproperties
• The first-order logic of hyperproperties
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties

Cited in

(21)

• Team semantics for the specification and verification of hyperproperties
• Propositional Dynamic Logic for Hyperproperties
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Model checking algorithms for hyperproperties (invited paper)
• Unification in Linear Modal Logic on Non-transitive Time with the Universal Modality
• Complexity results for modal logic with recursion via translations and tableaux
• Linear-time temporal answer set programming
• Runtime enforcement of hyperproperties
• The complexity of second-order HyperLTL
• Formal semantics of meta-level architectures: Temporal epistemic reflection
• Flavors of sequential information flow
• Centralized vs. decentralized monitors for hyperproperties
• Temporal team semantics revisited
• The complexity of second-order HyperLTL
• Complexity through translations for modal logic with recursion
• Unifying asynchronous logics for hyperproperties
• Explainability requirements as hyperproperties
• Information-flow interfaces
• Information-flow interfaces
• Second-order hyperproperties
• Predicate abstraction for hyperliveness verification

This page was built for publication: Unifying hyper and epistemic temporal logics

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