Abstract
The paper presents a structured translation from a static (bounded) subset of PROMELA/SPIN to the planning description language PDDL2.1. It exploits the representation of protocols as communicating finite state machines.
First, the state-space representation is defined to handle processes, queues, and shared variables. Second, each basic statement (assignment, input, etc.) is translated into a couple of predicates.
The deadlock detection problem is reformulated as an action planning problem and SPIN is compared to two action planners Metric-FF and MIPS on several benchmarks (e.g. leader election, dining philosophers, optical telegraph).
The difference to existing approaches is the direct use of planning tools. As a byproduct this introduces refined estimates for improved error detection in directed protocol validation.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
F. Bacchus and F. Kabanza. Using temporal logics to express search control knowledge for planning. Artificial Intelligence, 116:123–191, 2000.
G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Petterson, J. Romijn, and F. W. Vaandrager. Efficient guiding towards cost-optimality in uppaal. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2001.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science. Springer, 1999.
A. Blum and M. L. Furst. Fast planning through planning graph analysis. In International Joint Conferences on Artificial Intelligence (IJCAI), pages 1636–1642, 1995.
A. Cimatti and M. Roveri. Conformant planning via model checking. In European Conference on Planning (ECP), pages 21–33, 1999.
A. Cimatti, M. Roveri, and P. Traverso. Automatic OBDD-based generation of universal plans in non-deterministic domains. In National Conference on Artificial Intelligence (AAAI), pages 875–881, 1998.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
H. Dierks, G. Behrmann, and K. G. Larsen. Solving planning problems using real-time model checking (translating pddl3 into timed automata). In Artificial Intelligence Planning and Scheduling (AIPS)-Workshop on Temporal Planning, pages 30–39, 2002.
S. Edelkamp. Planning with pattern databases. In European Conference on Planning (ECP), 2001.
S. Edelkamp. Taming numbers and durations in the model checking integrated planning system. Journal of Artificial Research (JAIR), 2003. Submitted, A draft is available at PUK-Workshop 2002.
S. Edelkamp and M. Helmert. The model checking integrated planning system MIPS. AI-Magazine, pages 67–71, 2001.
S. Edelkamp, S. Leue, and A. Lluch-Lafuente. Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology (STTT), 2003.
R. Fikes and N. Nilsson. Strips: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2:189–208, 1971.
M. Fox and D. Long. PDDL2.1: An extension to PDDL for expressing temporal planning domains. Technical report, University of Durham, UK, 2001.
A. Gerevini and L. Schubert. Discovering state constraints in DISCOPLAN: Some new results. In National Conference on Artificial Intelligence (AAAI), pages 761–767, 2000.
A. Gerevini and I. Serina. LPG: a planner based on local search for planning graphs with action costs. In Artificial Intelligence Planning and Scheduling (AIPS), pages 13–22, 2002.
F. Giunchiglia and P. Traverso. Planning as model checking. In European Conference on Planning (ECP), pages 1–19, 1999.
Patrice Godefroid and Sarfraz Khurshid. Exploring very large state spaces using genetic algorithms. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2002.
P. E. Hart, N. J. Nilsson, and B. Raphael. A formal basis for heuristic determination of minimum path cost. IEEE Transactions on on Systems Science and Cybernetics, 4:100–107, 1968.
J. Hoey, R. Aubin, A. Hu, and C. Boutilier. Spudd: Stochastic planning using decision diagrams. In Conference on Uncertainty in Artificial Intelligence (UAI), 1999.
J. Hoffmann. Extending FF to numerical state variables. In European Conference on Artificial Intelligence, 2002.
J. Hoffmann and B. Nebel. Fast plan generation through heuristic search. Artificial Intelligence Research, 14:253–302, 2001.
G. J. Holzmann and M. H. Smith. Software model checking: Extracting verification models from source code. In Formal Description Techniques for Distributed Systems and Communication Protocols, Protocol Specification, Testing and Verification (FORTE/PSTV), pages 481–497, 1999.
Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1990.
Falk Hüffner, S. Edelkamp, H. Fernau, and R. Niedermeier. Finding optimal solutions to Atomix. In German Conference on Artificial Intelligence (KI), pages 229–243, 2001.
H. Kautz and B. Selman. Pushing the envelope: Planning propositional logic, and stochastic search. In National Conference on Artificial Intelligence (AAAI), pages 1194–1201, 1996.
R. E. Korf. Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence, 27(1):97–109, 1985.
J. Kvarnström, P. Doherty, and P. Haslum. Extending TALplanner with concurrency and ressources. In European Conference on Artificial Intelligence (ECAI), pages 501–505, 2000.
D. Long and M. Fox. Efficient implementation of the plan graph in STAN. Artificial Intelligence Research, 10:87–115, 1998.
D. McDermott. The 1998 AI Planning Competition. AI Magazine, 21(2), 2000.
J. Pearl. Heuristics. Addison-Wesley, 1985.
C. H. Yang and D. L. Dill. Validation with guided search of the state space. In Conference on Design Automation (DAC), pages 599–604, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Edelkamp, S. (2003). Promela Planning. In: Ball, T., Rajamani, S.K. (eds) Model Checking Software. SPIN 2003. Lecture Notes in Computer Science, vol 2648. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44829-2_13
Download citation
DOI: https://doi.org/10.1007/3-540-44829-2_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40117-9
Online ISBN: 978-3-540-44829-7
eBook Packages: Springer Book Archive