Experimental Evaluation of a Planning Language Suitable for Formal Verification

作者: Radu I. Siminiceanu , Rick W. Butler , César A. Muñoz

DOI: 10.1007/978-3-642-00431-5_9

关键词:

摘要: The marriage of model checking and planning faces two seemingly diverging alternatives: the need for a language expressive enough to capture complexity real-life applications, as opposed simple, yet robust be amenable exhaustive verification validation techniques. In an attempt reconcile these differences, we have designed abstract plan description language, ANMLite, inspired from Action Notation Modeling Language (ANML). We present basic concepts ANMLite well automatic translator checker SAL (Symbolic Analysis Laboratory). discuss various aspects specifying in terms constraints explore implications choosing logic behind specification constraints, rather than simply propose new language. Additionally, provide initial assessment efficiency search solutions problems. To this end, design test benchmark study scalability generated models complexity.

参考文章(19)
A. Lomuscio, S. Edelkamp, Model Checking and Artificial Intelligence ,(2008)
Stefan Edelkamp, None, Heuristic Search Planning with BDDs. PuK. ,(2000)
Ricky W. Butler, Cesar A. Munoz, An Abstract Plan Preparation Language ,(2006)
Ricky W. Butler, Radu I. Siminiceanu, Cesar A. Munoz, The Anmlite Language and Logic for Specifying Planning Problems ,(2013)
Hossein M. Sheini, Bart Peintner, Karem A. Sakallah, Martha E. Pollack, On Solving Soft Temporal Constraints Using SAT Techniques Principles and Practice of Constraint Programming - CP 2005. pp. 607- 621 ,(2005) , 10.1007/11564751_45
Charles Pecheur, Roberto Cavada, Alessandro Cimatti, Formal verification of diagnosability via symbolic model checking international joint conference on artificial intelligence. pp. 363- 369 ,(2003)
Jeremy Frank, Ari Jónsson, Constraint-Based Attribute and Interval Planning Constraints - An International Journal. ,vol. 8, pp. 339- 364 ,(2003) , 10.1023/A:1025842019552
Alessandro Cimatti, Enrico Giunchiglia, Fausto Giunchiglia, Paolo Traverso, Planning via Model Checking: A Decision Procedure for AR Lecture Notes in Computer Science. pp. 130- 142 ,(1997) , 10.1007/3-540-63912-8_81
Robert St-Aubin, Alan Hu, Craig Boutilier, Jesse Hoey, SPUDD: stochastic planning using decision diagrams uncertainty in artificial intelligence. pp. 279- 288 ,(1999)
Enrico Giunchiglia, Paolo Ferraris, Planning as Satisfiability in Nondeterministic Domains national conference on artificial intelligence. pp. 748- 753 ,(2000)