150 citations · 274 across the 7 of their papers we have counts for
7 papers
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
Alexandre David, Lasse Jacobsen, Morten Jacobsen +1
Timed-arc Petri nets (TAPN) are a well-known time extension of the Petri net model and several translations to networks of timed automata have been proposed for this model. We pres…
Statistical Model Checking for Stochastic Hybrid Systems
Alexandre David, Dehui Du, Kim G. Larsen +4
This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how…
UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata
Peter Bulychev, Alexandre David, Kim Gulstrand Larsen +4
This paper offers a survey of uppaalsmc, a major extension of the real-time verification tool uppaal. uppaalsmc allows for the efficient analysis of performance properties of netwo…
Controllers with Minimal Observation Power (Application to Timed Systems)
Peter Bulychev, Franck Cassez, Alexandre David +3
We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The…
Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach
Peter Bulychev, Alexandre David, Kim G. Larsen +2
This paper studies the problem of computing Nash equilibrium in wireless networks modeled by Weighted Timed Automata. Such formalism comes together with a logic that can be used to…
Distributed Parametric and Statistical Model Checking
Peter Bulychev, Alexandre David, Kim Guldstrand Larsen +2
Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if th…