Propositional Dynamic Logic for Hyperproperties

DOI10.4230/LIPICS.CONCUR.2020.50MaRDI QIDQ5089318zbMATH OpenOpenAlexFDO

Authors Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem

Publication date 18 July 2022

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

zbMATH Keywords

automatahyperlogicshyperpropertiesmodel checking

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• Algorithms for model checking HyperLTL and HyperCTL^*
• Alternating finite automata on -words
• Complete Axiomatizations for Reasoning about Knowledge and Time
• Complete Proof System for QPTL
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 6851935 (Why is no real title available?)
• scientific article; zbMATH DE number 1863182 (Why is no real title available?)
• Model checking propositional dynamic logic with all extras
• Parametric linear dynamic logic
• Propositional dynamic logic of regular programs
• Temporal logics in computer science. Finite-state systems
• Unifying hyper and epistemic temporal logics
• Weak alternating automata are not that weak

Cited in

(11)

• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Efficient loop conditions for bounded model checking hyperproperties
• Stack-aware hyperproperties
• Second-order hyperproperties
• Temporal team semantics revisited
• Deciding hyperproperties combined with functional specifications
• Temporal hyperproperties for population protocols
• Model checking omega-regular hyperproperties with AutoHyperQ
• Unifying asynchronous logics for hyperproperties
• Inquisitive team semantics of LTL
• Extensions of HyperLTL for asynchronous hyperproperties

This page was built for publication: Propositional Dynamic Logic for Hyperproperties

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