Reachability Problems
 
Reachability is a fundamental problem that appears in several different contexts: finite- and infinite-state concurrent systems, computational models like cellular automata and Petri nets, program analysis, discrete and continuous systems, time critical systems, hybrid systems, rewriting systems, probabilistic and parametric systems, and open systems modelled as games. In general reachability problem can be formulated as follows: Given a computational (potentially infinite state) system with a set of allowed rules or transformations, decide whether a certain state of a system is reachable from a given initial state of the system. The variants of such reachability problem may be appear as a result of additional constraints on the initial or final states, specific requirement for a reachability paths as well as for iterative reachability or changing the questions into analysis of winning strategies in infinite games or unavoidability of some dynamics. Typically, for a fixed system description given in some form (reduction rules, systems of equations, logical formulas, etc.) a reachability problem consists in checking whether a given set of target states can be reached starting from a fixed set of initial states. The set of target states can be represented explicitly or via some implicit representation (e.g., a system of equations, a set of minimal elements with respect to some ordering on the states). Sophisticated quantitative and qualitative properties can often be reduced to basic reachability questions. Decidability and complexity boundaries, algorithmic solutions, and efficient heuristics are all important aspects to be considered in this context. Algorithmic solutions are often based on different combinations of exploration strategies, symbolic manipulations of sets of states, decomposition properties, reduction to linear programming problems, and they often benefit from approximations, abstractions, accelerations and extrapolation heurisitics. Ad hoc solutions as well as solutions based on general purpose constraint solvers and deduction engines are often combined in order to balance efficiency and flexibility.http://en.wikipedia.org/wiki/Computational_modelhttp://en.wikipedia.org/wiki/Cellular_automatahttp://en.wikipedia.org/wiki/Petri_nethttp://en.wikipedia.org/wiki/Program_analysishttp://en.wikipedia.org/wiki/Hybrid_systemhttp://en.wikipedia.org/wiki/Rewriting_systemshapeimage_3_link_0shapeimage_3_link_1shapeimage_3_link_2shapeimage_3_link_3shapeimage_3_link_4shapeimage_3_link_5

Workshop on Reachability Problems

  1. •PR’15 in Warsaw, Poland , LNCS proceedings, Springer Verlag

  2. •RP'14 in Oxford, UK , LNCS proceedings, Springer Verlag

  3. •RP'13 in Uppsala, Sweden, LNCS proceedings, Springer Verlag

  4. •RP'12 in Bordeaux, France, LNCS proceedings, Volume 7550/2012, Springer Verlag

  5. •RP'11 in Genova, Italy, LNCS proceedings, Volume 6945/2011, Springer Verlag

  6. •RP'10 in Brno, Czech Republic, LNCS proceedings, Volume 6227/2010, Springer Verlag

  7. •RP'09 in Palaiseau, France, LNCS proceedings, Volume 5797/2009, Springer Verlag

  8. •RP'08 in Liverpool, UK, ENTCS proceedings, Volume 223, Elsevier

  9. •RP'07 in Turku, Finland, TUCS General Publication Serie, Volume 45,

                    Turku Centre for Computer Science