150 citations · 623 across the 65 of their papers we have counts for
4 papers · 2 filters
Lightweight Monte Carlo Verification of Markov Decision Processes with Rewards
Axel Legay, Sean Sedwards, Louis-Marie Traonouez
Markov decision processes are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightwei…
Homotopy Bisimilarity for Higher-Dimensional Automata
Uli Fahrenberg, Axel Legay
We introduce a new category of higher-dimensional automata in which the morphisms are functional homotopy simulations, i.e. functional simulations up to concurrency of independent…
Compositionality for Quantitative Specifications
Uli Fahrenberg, Jan Křetínský, Axel Legay +1
We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive…
Structural Refinement for the Modal nu-Calculus
Uli Fahrenberg, Axel Legay, Louis-Marie Traonouez
We introduce a new notion of structural refinement, a sound abstraction of logical implication, for the modal nu-calculus. Using new translations between the modal nu-calculus and…