Propositional Dynamic Logic for Hyperproperties

DOI10.4230/LIPIcs.CONCUR.2020.50OpenAlexW3081601885MaRDI QIDQ5089318

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

Publication date: 18 July 2022

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

zbMATH Keywords

automatamodel checkinghyperpropertieshyperlogics

Mathematics Subject Classification ID

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

Related Items

HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Parametric linear dynamic logic
• Alternating finite automata on \(\omega\)-words
• Propositional dynamic logic of regular programs
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Model checking propositional dynamic logic with all extras
• Temporal Logics in Computer Science
• Unifying Hyper and Epistemic Temporal Logics
• Weak alternating automata are not that weak
• Complete Axiomatizations for Reasoning about Knowledge and Time
• Complete Proof System for QPTL