CISPA
Browse
View of Non-deterministic Planning for Hyperproperty Verification.pdf (2.8 MB)

Non-deterministic Planning for Hyperproperty Verification

Download (2.8 MB)
conference contribution
posted on 2024-06-20, 08:57 authored by Raven BeutnerRaven Beutner, Bernd FinkbeinerBernd Finkbeiner
Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem. We implement our encoding in a prototype verification tool and report on encouraging experimental results.

History

Editor

Bernardini S ; Muise C

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Conference on Automated Planning and Scheduling (ICAPS)

Journal

Proceedings of the International Conference on Automated Planning and Scheduling

Volume

34

Page Range

25-30

Publisher

Association for the Advancement of Artificial Intelligence (AAAI)

Open Access Type

  • Unknown

BibTeX

@inproceedings{Beutner:Finkbeiner:2024, title = "Non-deterministic Planning for Hyperproperty Verification", author = "Beutner, Raven" AND "Finkbeiner, Bernd", editor = "Bernardini, Sara" AND "Muise, Christian", year = 2024, month = 5, journal = "Proceedings of the International Conference on Automated Planning and Scheduling", pages = "25--30", publisher = "Association for the Advancement of Artificial Intelligence (AAAI)", issn = "2334-0843", doi = "10.1609/icaps.v34i1.31457" }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC