Title :
Model checking based service delivery planning
Author :
Soeanu, Andrei ; Ray, Sambaran ; Debbabi, Mourad ; Berger, Josef ; Boukhtouta, Abdeslem ; Ghanmi, Ahmed
Author_Institution :
Concordia Univ., Montreal, QC, Canada
fDate :
April 29 2012-May 2 2012
Abstract :
Service delivery planning may often involve plan specific ordering or sequencing especially in non-euclidean transit environments. Common approaches for vehicle routing fall short in adequately handling compound ad-hoc plan dependent constraints. We address multi-agent service provisioning by starting from different initial nodes of shared irregular transport graphs. We employ concurrent and interleaved dynamics composition to capture agent based service delivery problems as transition systems and related goal state properties that can be the subject of symbolic model checking. Formally verifying the negation of the goal state property allows to generate a counter example such that, if it exists, the route allocation planning problem finds a solution. The state explosion is mitigated by bounded model checking that has the additional advantage of providing counter examples of minimal length which correspond to minimized agent tours under a cost bound.
Keywords :
computational complexity; constraint handling; formal verification; graph theory; multi-agent systems; transportation; NP-hard problem; agent based service delivery problem; agent tour minimization; bounded model checking; compound ad-hoc plan dependent constraint handling; concurrent dynamics composition; cost bound; formal verification; goal state property negation; interleaved dynamics composition; multiagent service provisioning; nonEuclidean transit environment; plan specific ordering; plan specific sequencing; route allocation planning problem; service delivery planning; shared irregular transport graph; state explosion mitigation; symbolic model checking; transition system; vehicle routing; Encoding; Fuels; Planning; Radiation detectors; Vehicle dynamics; Vehicles; Intelligent Transportation; Symbolic Model Checking; Tour Planning; Traveling Repairman Problem;
Conference_Titel :
Electrical & Computer Engineering (CCECE), 2012 25th IEEE Canadian Conference on
Conference_Location :
Montreal, QC
Print_ISBN :
978-1-4673-1431-2
Electronic_ISBN :
0840-7789
DOI :
10.1109/CCECE.2012.6334956