Propositional Dynamic Logic for Hyperproperties

DOI10.4230/LIPICS.CONCUR.2020.50OpenAlexW3081601885MaRDI QIDQ5089318FDOQ5089318

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

model checkingautomatahyperpropertieshyperlogics

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Propositional dynamic logic of regular programs
• Model checking propositional dynamic logic with all extras
• Alternating finite automata on \(\omega\)-words
• Weak alternating automata are not that weak
• Complete Axiomatizations for Reasoning about Knowledge and Time
• Parametric linear dynamic logic
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Temporal logics in computer science. Finite-state systems
• Complete Proof System for QPTL
• Unifying Hyper and Epistemic Temporal Logics

Cited In (6)

• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Efficient loop conditions for bounded model checking hyperproperties
• Deciding hyperproperties combined with functional specifications
• Temporal team semantics revisited
• Stack-aware hyperproperties
• Second-order 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)