Algorithms for model checking HyperLTL and HyperCTL\(^*\)

DOI10.1007/978-3-319-21690-4_3zbMath1381.68161OpenAlexW1213177963MaRDI QIDQ1702908

Bernd Finkbeiner, César Sánchez, Markus N. Rabe

Publication date: 1 March 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-21690-4_3

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Timed hyperproperties, Model-Checking HyperLTL for Pushdown Systems, A temporal logic for asynchronous hyperproperties, Constraint-based relational verification, Runtime enforcement of hyperproperties, HyperPCTL model checking by probabilistic decomposition, CoSMed: a confidentiality-verified social media platform, HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems, Is Your Software on Dope?, Unnamed Item, Program Repair for Hyperproperties, Model Checking Data Flows in Concurrent Network Updates, Finite-word hyperlanguages, Team semantics for the specification and verification of hyperproperties, Model checking algorithms for hyperproperties (invited paper), Compositional model checking for multi-properties, Monitoring hyperproperties, CoCon: a conference management system with formally verified document confidentiality, Bounded model checking for hyperproperties, Synthesis from hyperproperties, Propositional Dynamic Logic for Hyperproperties, Model checking hyperproperties for Markov decision processes, Good-for-Game QPTL: An Alternating Hodges Semantics