25 citations · 56 across the 15 of their papers we have counts for
6 papers · 1 filter
Synthesizing Approximate Implementations for Unrealizable Specifications
Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah
The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bo…
Approximate Automata for Omega-Regular Languages
Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah
Automata over infinite words, also known as omega-automata, play a key role in the verification and synthesis of reactive systems. The spectrum of omega-automata is defined by two…
Canonical Representations of k-Safety Hyperproperties
Bernd Finkbeiner, Lennart Haas, Hazem Torfah
Hyperproperties elevate the traditional view of trace properties form sets of traces to sets of sets of traces and provide a formalism for expressing information-flow policies. For…
Explainable Reactive Synthesis
Tom Baumeister, Bernd Finkbeiner, Hazem Torfah
Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. The main advantage of synthesis is that it is automatic. The…
SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System
Sumukh Shivakumar, Hazem Torfah, Ankush Desai +1
We present an implementation of SOTER, a run-time assurance framework for building safe distributed mobile robotic (DMR) systems, on top of the Robot Operating System (ROS). The sa…
Probabilistic Hyperproperties of Markov Decision Processes
Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah
Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include informat…