4 papers
Disintegration Temporal Logic for Probabilistic Hyperproperties
Mishel Carelli, Bernd Finkbeiner
We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-int…
Loop Termination and Generalized Collatz Sequences
Mishel Carelli
Linear-constraint loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an inf…
Closure and Complexity of Temporal Causality
Mishel Carelli, Bernd Finkbeiner, Julian Siber
Temporal causality defines what property causes some observed temporal behavior (the effect) in a given computation, based on a counterfactual analysis of similar computations. In…
CTL* Verification and Synthesis using Existential Horn Clauses
Mishel Carelli, Orna Grumberg
This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to specifications, based on translation to E…