MFCS & CSL 2010
Petrov - Cathedral of St. Peter, Brno

Contacts

General questions about organization, registration, accomodation, etc., should be sent to

xrebok@fi.muni.cz

Program-related questions should be directed to program committee chairs.

More details

Games and Probabilistic Models in Formal Verification

Aim

Formal methods are widely used in development and analysis of complex systems such as aircraft flight control systems, controllers of industrial processes, biological processes etc. These systems usually exhibit features such as randomness, interaction and parallelism. Probabilistic and game theoretic models are especially well suited for capturing these features and therefore there is a need to develop such models and methods for their analysis. The goal of this workshop is to bring together researchers with interest in probabilistic and game theoretic methods in formal verification.

Topics

  • algorithms for finite and infinite games
  • automata theory and games
  • timed games
  • probabilistic models for verification
  • decision processes and stochastic games
  • logics for probabilistic models and games
  • probabilistic model checking

Invited Speakers

Submissions

GPMFV 2010 provides a forum for presentations of recent results in the above areas. We impose no restriction on previous or future publication of presented results. The selection of presentations will be based on one-page abstracts submitted via GPMFV 2010 submission page.

Important Dates

  • Submission deadline for presentations: 10 May 2010
  • Notification: 31 May 2010
  • Workshop: 28 August 2010

Program

08:30-09:20 J. Esparza. Analysing time and memory consumption in stochastic systems with process creation (invited talk)
09:20-09:45 V. Brozek. One-Counter Stochastic Games
09:45-10:10 J. Esparza, A. Gaiser and S. Kiefer. Computing Least Fixed Points of Probabilistic Systems of Polynomials
10:10-10:30 Coffee break
10:30-11:20 M. Groesser. Tossing coins in omega-automata (invited talk)
11:20-11:45 P. Cerny, T. Henzinger and A. Radhakrishna. Quantitative Simulation Games
11:45-12:10 P. Jancar. Bisimulation Game on Pushdown Automata
12:10-14:00 Lunch
14:00-14:50 T. Brihaye. Probabilistic and topological semantics for timed automata (invited talk)
14:50-15:15 A. Trivedi, V. Forejt, M. Kwiatkowska and G. Norman. Expected Reachability-Time Games
15:15-15:40 M. Rabe. Time-Bounded Reachability in Continuous-time Stochastic Games
15:40-16:00 Coffee break
16:00-16:50 H. Gimbert. Algorithms for Stochastic Games with Partial Observation (invited talk)
16:50-17:15 K. A. Hansen. Complexity Results for Concurrent Reachability Games
17:15-17:40 M. Mio. Products and CoProducts of Two Player Stochastic Games

Program Committee