This talk will provide an overview of work that I have done with Hana Chockler, Orna Kupferman, and Judea Pearl [1, 2, 10, 9] on defining notions such as causality, explanation, ...
Spectral expansion and matrix analytic methods are important solution mechanisms for matrix polynomial equations. These equations are encountered in the steady-state analysis of M...
Stochastic orders can be applied to Markov reward models and used to aggregate models, while introducing a bounded error. Aggregation reduces the number of states in a model, miti...
The time-bounded reachability problem for continuoustime Markov chains (CTMCs) amounts to determine the probability to reach a (set of) goal state(s) within a given time span, suc...
New mobile access networks provide reasonable high bandwidth to allow true internet access. This paper models two dominant applications of those networks. One application, WAP, is...
LiQuor is a tool for verifying probabilistic reactive systems modelled Probmela programs, which are terms of a probabilistic guarded command language with an operational semantics...
A concurrent reachability game is a two-player game played on a graph: at each state, the players simultaneously and independently select moves; the two moves determine jointly a ...
Krishnendu Chatterjee, Luca de Alfaro, Thomas A. H...
Abstract. We present a compositional theory of system verification, where specifications assign real-numbered costs to systems. These costs can express a wide variety of quantita...
Krishnendu Chatterjee, Luca de Alfaro, Marco Faell...