214:
105:, logical formulas, etc.) a reachability problem consists of 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.
252:, is an annual academic conference which gathers together researchers from diverse disciplines and backgrounds interested in reachability problems that appear in algebraic structures, computational models, hybrid systems, infinite games, logic and verification. The workshop tries to fill the gap between results obtained in different fields but sharing common mathematical structure or conceptual difficulties.
20:
154:, more precisely in classical planning, one is interested in knowing if one can attain a state from an initial state from a description of actions. The description of actions defines a graph of implicit states, which is of exponential size in the size of the description.
113:
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, or reduction to
169:
The reachability problem in a Petri net is decidable. Since 1976, it is known that this problem is EXPSPACE-hard. There are results on how much to implement this problem in practice. In 2018, the problem was shown to be a
268:
Giorgio
Delzanno, Igor Potapov (Eds.): Reachability Problems - 5th International Workshop, RP 2011, Genoa, Italy, September 28â30, 2011. Proceedings. Lecture Notes in Computer Science 6945, Springer 2011,
90:
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.
135:
The reachability problem in an oriented graph described explicitly is NL-complete. Reingold, in a 2008 article, proved that the reachability problem for a non-oriented graph is in LOGSPACE.
118:
problems, and they often benefit from approximations, abstractions, accelerations and extrapolation heuristics. Ad hoc solutions as well as solutions based on general purpose
94:
Variants of the reachability problem may result from additional constraints on the initial or final states, specific requirement for reachability paths as well as for
421:
Czerwinski, Wojciech; Lasota, Slawomir; Lazic, Ranko; Leroux, Jerome; Mazowiecki, Filip (2019-04-11). "The
Reachability Problem for Petri Nets is Not Elementary".
287:
493:
98:
reachability or changing the questions into analysis of winning strategies in infinite games or unavoidability of some dynamics.
473:
405:
338:
274:
157:
In symbolic model checking, the model (the underlying graph) is described with the aid of a symbolic representation such as
249:
544:
224:
74:
392:. Lecture Notes in Computer Science. Vol. 3607. Berlin, Heidelberg: Springer. pp. 149â164.
295:
158:
190:
198:
171:
23:
The reachability problem consists of attaining a final situation from an initial situation.
30:
is a fundamental problem that appears in several different contexts: finite- and infinite-
8:
122:
and deduction engines are often combined in order to balance efficiency and flexibility.
102:
70:
38:
381:
518:
451:
422:
344:
194:
175:
115:
34:
469:
401:
334:
270:
119:
42:
382:"Petri Net Reachability Checking is Polynomial with Optimal Abstraction Hierarchies"
348:
323:
Proceedings of the thirteenth annual ACM symposium on Theory of computing - STOC '81
461:
393:
326:
62:
50:
248:
The
International Conference on Reachability Problems series, previously known as
498:
465:
178:
54:
443:
385:
362:
139:
101:
Typically, for a fixed system description given in some form (reduction rules,
31:
538:
517:. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS).
106:
66:
58:
325:. New York, NY, USA: Association for Computing Machinery. pp. 238â246.
330:
448:
2021 IEEE 62nd Annual
Symposium on Foundations of Computer Science (FOCS)
243:
78:
19:
397:
318:
213:
369:. Technical Report 62. Department of Computer Science, Yale University.
110:
95:
46:
444:"The Reachability Problem for Petri Nets is Not Primitive Recursive"
523:
456:
427:
151:
494:"An Easy-Sounding Problem Yields Numbers Too Big for Our Universe"
109:
and complexity boundaries, algorithmic solutions, and efficient
515:
Reachability in Vector
Addition Systems is Ackermann-complete
319:"An algorithm for the general Petri net reachability problem"
420:
142:, reachability corresponds to a property of liveliness.
244:
International
Conference on Reachability Problems (RP)
512:
125:
367:
513:CzerwiĆski, Wojciech; Orlikowski, Ćukasz (2021).
536:
390:Abstraction, Reformulation and Approximation
184:
174:. In 2022 it was shown to be complete for
522:
455:
426:
491:
285:
145:
130:
18:
537:
441:
379:
361:
288:"Undirected Connectivity in Log-Space"
487:
485:
316:
208:
16:Problem in math and computer science
13:
14:
556:
492:Brubaker, Ben (4 December 2023).
482:
435:
250:Workshop on Reachability Problems
126:Variants of reachability problems
442:Leroux, Jerome (February 2022).
212:
204:
292:omereingold.files.wordpress.com
55:discrete and continuous systems
506:
414:
373:
355:
310:
279:
262:
88:can be formulated as follows:
1:
317:Mayr, Ernst W. (1981-05-11).
286:Reingold, Omer (3 May 2008).
255:
164:
466:10.1109/FOCS52979.2021.00121
450:. IEEE. pp. 1241â1252.
7:
10:
561:
384:. In Zucker, Jean-Daniel;
197:-complete and therefore a
57:, time critical systems,
189:In 2022 reachability in
159:binary decision diagrams
191:vector addition systems
185:Vector addition systems
221:This section is empty.
24:
545:Theory of computation
380:KĂŒngas, Peep (2005).
331:10.1145/800076.802477
199:nonelementary problem
172:nonelementary problem
146:Finite implicit graph
131:Finite explicit graph
22:
103:systems of equations
86:reachability problem
39:computational models
398:10.1007/11527862_11
176:Ackermann function
120:constraint solvers
116:linear programming
35:concurrent systems
25:
475:978-1-6654-2055-6
407:978-3-540-31882-8
340:978-1-4503-7392-0
275:978-3-642-24287-8
241:
240:
63:rewriting systems
43:cellular automata
552:
529:
528:
526:
510:
504:
503:
489:
480:
479:
459:
439:
433:
432:
430:
418:
412:
411:
377:
371:
370:
359:
353:
352:
314:
308:
307:
305:
303:
294:. Archived from
283:
277:
266:
236:
233:
223:You can help by
216:
209:
193:was shown to be
51:program analysis
560:
559:
555:
554:
553:
551:
550:
549:
535:
534:
533:
532:
511:
507:
499:Quanta Magazine
490:
483:
476:
440:
436:
419:
415:
408:
386:Saitta, Lorenza
378:
374:
360:
356:
341:
315:
311:
301:
299:
284:
280:
267:
263:
258:
246:
237:
231:
228:
207:
187:
179:time complexity
167:
148:
133:
128:
84:In general the
17:
12:
11:
5:
558:
548:
547:
531:
530:
505:
481:
474:
434:
413:
406:
372:
354:
339:
309:
278:
260:
259:
257:
254:
245:
242:
239:
238:
219:
217:
206:
203:
186:
183:
166:
163:
147:
144:
140:model checking
132:
129:
127:
124:
59:hybrid systems
15:
9:
6:
4:
3:
2:
557:
546:
543:
542:
540:
525:
520:
516:
509:
501:
500:
495:
488:
486:
477:
471:
467:
463:
458:
453:
449:
445:
438:
429:
424:
417:
409:
403:
399:
395:
391:
387:
383:
376:
368:
364:
358:
350:
346:
342:
336:
332:
328:
324:
320:
313:
298:on 2007-06-15
297:
293:
289:
282:
276:
272:
265:
261:
253:
251:
235:
226:
222:
218:
215:
211:
210:
205:Open problems
202:
200:
196:
192:
182:
180:
177:
173:
162:
160:
155:
153:
143:
141:
136:
123:
121:
117:
112:
108:
104:
99:
97:
92:
91:
87:
82:
80:
76:
73:systems, and
72:
68:
67:probabilistic
64:
60:
56:
52:
48:
44:
40:
36:
33:
29:
21:
514:
508:
497:
447:
437:
416:
389:
375:
366:
357:
322:
312:
300:. Retrieved
296:the original
291:
281:
264:
247:
229:
225:adding to it
220:
188:
168:
156:
149:
137:
134:
107:Decidability
100:
93:
89:
85:
83:
77:modelled as
75:open systems
28:Reachability
27:
26:
524:2104.13866
457:2104.12695
428:1809.07115
363:Lipton, R.
302:9 December
256:References
232:April 2013
165:Petri nets
111:heuristics
71:parametric
47:Petri nets
195:Ackermann
96:iterative
539:Category
388:(eds.).
365:(1976).
349:15409115
152:planning
472:
404:
347:
337:
273:
519:arXiv
452:arXiv
423:arXiv
345:S2CID
79:games
41:like
32:state
470:ISBN
402:ISBN
335:ISBN
304:2021
271:ISBN
69:and
45:and
462:doi
394:doi
327:doi
227:.
150:In
138:In
541::
496:.
484:^
468:.
460:.
446:.
400:.
343:.
333:.
321:.
290:.
201:.
181:.
161:.
81:.
65:,
61:,
53:,
49:,
37:,
527:.
521::
502:.
478:.
464::
454::
431:.
425::
410:.
396::
351:.
329::
306:.
234:)
230:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
