25 citations · 56 across the 15 of their papers we have counts for
18 papers
Statistical Verification of Quantitative Hyperproperties: Beyond Boolean Quantification
Amir M. Ahmadian, Hazem Torfah
Formalisms for hyperproperties provide a solid foundation for studying the verification problem across classes of relational properties, such as those in information flow control (…
Learning Robust Markov Models for Safe Runtime Monitoring
Antonina Skurka, Luko van der Maas, Sebastian Junges +1
We present a model-based approach to learning robust runtime monitors for autonomous systems. Runtime monitors play a crucial role in raising the level of assurance by observing sy…
Querying Labeled Time Series Data with Scenario Programs
Edward Kim, Devan Shanker, Varun Bharadwaj +5
Simulation-based testing has become a crucial complement to road testing for ensuring the safety of cyber physical systems (CPS). As a result, significant research efforts have bee…
Locally Pareto-Optimal Interpretations for Black-Box Machine Learning Models
Aniruddha Joshi, Supratik Chakraborty, S Akshay +3
Creating meaningful interpretations for black-box machine learning models involves balancing two often conflicting objectives: accuracy and explainability. Exploring the trade-off…
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
Hazem Torfah, Shetal Shah, Supratik Chakraborty +2
We present a new multi-objective optimization approach for synthesizing interpretations that "explain" the behavior of black-box machine learning models. Constructing human-underst…
Runtime Monitoring for Markov Decision Processes
Sebastian Junges, Hazem Torfah, Sanjit A. Seshia
We investigate the problem of monitoring partially observable systems with nondeterministic and probabilistic dynamics. In such systems, every state may be associated with a risk,…
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…
Model Checking Quantitative Hyperproperties
Bernd Finkbeiner, Christopher Hahn, Hazem Torfah
Hyperproperties are properties of sets of computation traces. In this paper, we study quantitative hyperproperties, which we define as hyperproperties that express a bound on the n…
The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
Hadas Kress-Gazit, Hazem Torfah
In formal synthesis of reactive systems an implementation of a system is automatically constructed from its formal specification. The great advantage of synthesis is that the resul…
Synthesizing Skeletons for Reactive Systems
Bernd Finkbeiner, Hazem Torfah
We present an analysis technique for temporal specifications of reactive systems that identifies, on the level of individual system outputs over time, which parts of the implementa…
The Density of Linear-time Properties
Bernd Finkbeiner, Hazem Torfah
Finding models for linear-time properties is a central problem in verification and planning. We study the distribution of linear-time models by investigating the density of linear-…
Real-time Stream-based Monitoring
Peter Faymonville, Bernd Finkbeiner, Maximilian Schwenger +1
We introduce RTLola, a new stream-based specification language for the description of real-time properties of reactive systems. The key feature is the integration of sliding window…
The Complexity of Counting Models of Linear-time Temporal Logic
Hazem Torfah, Martin Zimmermann
We determine the complexity of counting models of bounded size of specifications expressed in Linear-time Temporal Logic. Counting word models is #P-complete, if the bound is given…