36 papers
Noise-aware Verification and Synthesis of Quantum Programs
Stefanie Muroya, Krishnendu Chatterjee, Thomas A. Henzinger
While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hard…
Shielding for Higher-Order Safety
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner
Safety shields are runtime enforcement mechanisms that restrict the actions of a controller to guarantee safety. Classical shields are usually synthesised for state predicates: the…
Algorithms for Equilibria in Concurrent Stopping Games
Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini
Concurrent games are a standard model for multi-agent systems, with Nash equilibrium as their central solution concept. The associated \emph{constrained existence problem}---does a…
Formal Verification of Continuous-Variable Quantum Programs
Stefanie Muroya, Thomas A. Henzinger
We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for conti…
Generalized Bidding Games: Where Bidding and Stochastic Games Meet
Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady +2
Two-player games on graphs are a classical framework for analyzing strategic decision making. In turn-based games, two players move a token along the edges of the graph, and the ri…
Monitoring Discounted Sum Properties
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner +1
Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obsc…