Borzoo Bonakdarpour

Wei Zhao, Borzoo Bonakdarpour

We introduce a decentralized and online path planning technique for a network of unmanned aerial vehicles (UAVs) in the presence of weather disturbances. In our problem setting, the group of UAVs are required to collaboratively visit a set of goals scattered in a 2-dimensional area. Each UAV will have to spend energy to reach these goals, but due to unforeseen disturbances, the required energy may vary over time and does not necessarily conform with the initial forecast and/or pre-computed optimal paths. Thus, we are dealing with two fundamental interrelated problems to find a global optimum at each point of time: (1) energy consumption prediction based on disturbances and, hence, online path replanning, and (2) distributed agreement among all UAVs to divide the remaining unvisited goals based on their positions and energy requirements. Our approach consists of four main components: (i) a distributed algorithm that periodically divides the unvisited goals among all the UAVs based on the current energy requirements of the UAVs, (ii) a local (i.e., UAV-level) $\AStar$-based algorithm that computes the {\em desirable} path for each UAV to reach the nodes assigned to it, (iii) a local PID controller that {\em predicts} the inputs to the UAV (i.e., thrust and moments), and (iv) a planner that computes the required energy and the replanning time period. We validate our proposed solution through a rich set of simulations and show that our approach is significantly more efficient than a best-effort algorithm that directs each idle UAV to visit the closest unvisited goal.

Lina Gerlach, Tobias Winkler, Erika Ábrahám et al.

Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characterizations of security and privacy policies. However, model checking for existing probabilistic hyperlogics, such as HyperPCTL and PHL, is undecidable in Markov decision processes (MDPs). In this paper, we study an underexplored problem: the verification of fragments of probabilistic hyperproperties that relate the probabilities of different events to each other, possibly across independent executions of an MDP. Representative verification questions include: Can two different target states be reached from the same initial state with the same probability? (different events), Can a given target state be reached from two different initial states with the same probability? (same event, independent executions), and natural combinations of these forms. Besides reachability, our relational probabilistic properties cover safety, Büchi, and coBüchi objectives. They can also be combined conjunctively, thereby generalizing standard multi-objective MDP properties. We provide efficient algorithms for relevant classes of relational properties, while proving computational hardness and completeness results for others. An implementation of our approach outperforms solvers for more general probabilistic hyperlogics by orders of magnitude on the subset of their benchmarks that lies within our fragment.

Tzu-Han Hsu, Arshia Rafieioskouei, Borzoo Bonakdarpour

Reward shaping in multi-agent reinforcement learning (MARL) for complex tasks remains a significant challenge. Existing approaches often fail to find optimal solutions or cannot efficiently handle such tasks. We propose HYPRL, a specification-guided reinforcement learning framework that learns control policies w.r.t. hyperproperties expressed in HyperLTL. Hyperproperties constitute a powerful formalism for specifying objectives and constraints over sets of execution traces across agents. To learn policies that maximize the satisfaction of a HyperLTL formula $φ$, we apply Skolemization to manage quantifier alternations and define quantitative robustness functions to shape rewards over execution traces of a Markov decision process with unknown transitions. A suitable RL algorithm is then used to learn policies that collectively maximize the expected reward and, consequently, increase the probability of satisfying $φ$. We evaluate HYPRL on a diverse set of benchmarks, including safety-aware planning, Deep Sea Treasure, and the Post Correspondence Problem. We also compare with specification-driven baselines to demonstrate the effectiveness and efficiency of HYPRL.

Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale et al.

We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

Tzu-Han Hsu, Cesar Sanchez, Borzoo Bonakdarpour

Hyperproperties are properties of systems that relate multiple computation traces, including security and concurrency properties. This paper introduces a bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL, which - to the best of our knowledge - is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. HyperLTL allows explicit and simultaneous quantification over traces and describes properties that involves multiple traces and, hence, our BMC approach naturally reduces to QBF solving. We report on successful and efficient model checking, implemented in a tool called HyperQube, of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and testing.

Erika Abraham, Ezio Bartocci, Borzoo Bonakdarpour et al.

We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic \HyperPCTL, which has been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize HyperPCTL by allowing explicit and simultaneous quantification over schedulers and probabilistic computation trees and show that it can express important quantitative requirements in security and privacy. We show that HyperPCTL model checking over MDPs is in general undecidable for quantification over probabilistic schedulers with memory, but restricting the domain to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language and evaluate its performance.

Borzoo Bonakdarpour, Sarai Sheinvald

Hyperproperties lift conventional trace properties from a set of execution traces to a set of sets of execution traces. Hyperproperties have been shown to be a powerful formalism for expressing and reasoning about information-flow security policies and important properties of cyber-physical systems such as sensitivity and robustness, as well as consistency conditions in distributed computing such as linearizability. Although there is an extensive body of work on automata-based representation of trace properties, we currently lack such characterization for hyperproperties. We introduce hyperautomata for em hyperlanguages, which are languages over sets of words. Essentially, hyperautomata allow running multiple quantified words over an automaton. We propose a specific type of hyperautomata called nondeterministic finite hyperautomata (NFH), which accept regular hyperlanguages. We demonstrate the ability of regular hyperlanguages to express hyperproperties for finite traces. We then explore the fundamental properties of NFH and show their closure under the Boolean operations. We show that while nonemptiness is undecidable in general, it is decidable for several fragments of NFH. We further show the decidability of the membership problem for finite sets and regular languages for NFH, as well as the containment problem for several fragments of NFH. Finally, we introduce learning algorithms based on Angluin's L-star algorithm for the fragments NFH in which the quantification is either strictly universal or strictly existential.

Sandro Stucki, César Sánchez, Gerardo Schneider et al.

Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. We first show that black-box monitoring of HyperLTL is in general unfeasible, and suggest a gray-box approach. Gray-box monitoring implies performing analysis of the system at run-time, which brings new limitations to monitorabiliy (the feasibility of solving the monitoring problem). Thus, as another contribution of this paper we refine the classic notions of monitorability, both for trace properties and hyperproperties, taking into account the computability of the monitor. We then apply our approach to monitor a privacy hyperproperty called distributed data minimality, expressed as a HyperLTL property, by using an SMT-based static verifier at runtime.

Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour et al.

Hyperproperties have shown to be a powerful tool for expressing and reasoning about information-flow security policies. In this paper, we investigate the problem of statistical model checking (SMC) for hyperproperties. Unlike exhaustive model checking, SMC works based on drawing samples from the system at hand and evaluate the specification with statistical confidence. The main benefit of applying SMC over exhaustive techniques is its efficiency and scalability. To reason about probabilistic hyperproperties, we first propose the temporal logic HyperPCLT* that extends PCTL* and HyperPCTL. We show that HyperPCLT* can express important probabilistic information-flow security policies that cannot be expressed with HyperPCTL. Then, we introduce SMC algorithms for verifying HyperPCLT* formulas on discrete-time Markov chains, based on sequential probability ratio tests (SPRT) with a new notion of multi-dimensional indifference region. Our SMC algorithms can handle both non-nested and nested probability operators for any desired significance level. To show the effectiveness of our technique, we evaluate our SMC algorithms on four case studies focused on information security: timing side-channel vulnerability in encryption, probabilistic anonymity in dining cryptographers, probabilistic noninterference of parallel programs, and the performance of a randomized cache replacement policy that acts as a countermeasure against cache flush attacks.

Fathiyeh Faghih, Borzoo Bonakdarpour, Sebastien Tixeuil et al.

In this paper, we introduce an SMT-based method that automatically synthesizes a distributed self-stabilizing protocol from a given high-level specification and network topology. Unlike existing approaches, where synthesis algorithms require the explicit description of the set of legitimate states, our technique only needs the temporal behavior of the protocol. We extend our approach to synthesize ideal-stabilizing protocols, where every state is legitimate. We also extend our technique to synthesize monotonic-stabilizing protocols, where during recovery, each process can execute an most once one action. Our proposed methods are fully implemented and we report successful synthesis of well-known protocols such as Dijkstra's token ring, a self-stabilizing version of Raymond's mutual exclusion algorithm, ideal-stabilizing leader election and local mutual exclusion, as well as monotonic-stabilizing maximal independent set and distributed Grundy coloring.