8th International Workshop on Reachability Problems (RP2014)

      22 – 24 September 2014, Oxford


Monday 22nd September

9.00-10.00: Invited Talk – Algorithms for Branching Markov Decision Processes. Kousha Etessami.

10.00-10.30: Reachability in MDPs: Refining Convergence of Value Iteration. Serge Haddad and Benjamin Monmege.

10.30-11.00: Coffee Break.

11.00-11.30: Parameter Synthesis for Timed Automata using Stochastic Game Abstractions. Aleksandra Jovanovic and Marta Kwiatkowska.

11.30-12.00: Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems. Ahmed Mahdi and Martin Fränzle.

12.00-12.30: On the Expressiveness of Metric Temporal Logic over Bounded Timed Words. Hsi-Ming Ho.

12.30-14.00: Lunch

14:00-15.00: Invited Talk- Complexity Bounds for Ordinal-Based Termination. Sylvain Schmitz.

15.00-15.30: On Functions Weakly Computable by Petri Nets and Vector Addition Systems. Jerome Leroux and Philippe Schnoebelen.

15.30-16.00: Coffee Break

16.00-16.30: Mean-payoff Games with Partial-Observation. Paul Hunter, Guillermo Perez and Jean-Francois Raskin.

16.30-17.00: Synthesising Succinct Strategies in Safety and Rechability Games. Gilles Geeraerts, Joël Goossens and Amélie Stainer.

17.00-17.30: Regular Strategies In Pushdown Reachability Games. Arnaud Carayol and Matthew Hague.

Tuesday 23rd September

9.00-10.00: Invited Talk – On the Subtle Interaction Between Reachability and Liveness. Byron Cook.

10.00-10.30: Effective Bounds on the Podelski-Rybalchenko Termination Theorem. Stefano Berardi, Paulo Oliva, and Silvia Stelia.

10.30-11.00: Coffee Break

11.00-11.30: Trace Inclusion for One-Counter Nets Revisited. Piotr Hofman and Patrick Totzke.

11-30-12.00: Integer Vector Addition Systems with States. Christoph Haase and Simon Halfon.

12:00-12.30: Equivalence Between Model-Checking Flat Counter Systems and Presburger Arithmetic. Stéphane Demri, Amit Kumar Dhar and Arnaud Sangnier.

12.30-14.00: Lunch

14.00-15.00: Invited Talk – Walking With Data: Where Does it Stop? Anca Muscholl.

15.00-15.30: Parameterized Verification of Communicating Automata under Context Bounds. Benedikt Bollig, Paul Gastin and Jana Schubert.

15.30-16.00: Coffee Break

16.00-16.30: Dynamical System Model (In)validation: A Dual to Reachability. James Anderson.

16.30-17.00: On The Complexity of Bounded Time Reachability for Piecewise Affine Systems. Hugo Bazille, Olivier Bournez, Walid Gomaa and Amaury Pouly.

17.00-17.30: Reachability and Mortality Problems for Hierarchical PCDs. Paul Bell, Shang Chen and Lisa Jackson.

Wednesday 24th September

9.00-9.30: Transformation-based Compositional Verification of Assumption-Commitment Properties. Ahmed Mahdi, Bernd Westphal and Martin Fränzle.

9.30-10.00: Compositional Reachability in Petri Nets.  Julian Rathke, Pawel Sobocinski and Owen Stephens.

10.00-10.30: Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations. Giorgio Delzanno and Jan Stückrath.

10.30-11.00: Coffee Break

11.00-11.30: On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability. Igor Konnov, Helmut Veith, and Josef Widder.

11.30-12.00: Utilizing Colored Petri Nets for Design Space Exploration of Asynchronous Microprocessors. Lei Wang, Yongwen Wang, Luo Li, Jun Gao, and Qiang Dou.

12.00-12.30: Reachability in pushdown register automata.  Andrzej Murawski, Steven Ramsay, Nikos Tzevelekos.kousha