"Eesti Teadusfondi uurimistoetus" projekt ETF7667
ETF7667 "Mudeli-põhine plaanurite süntees mittedeterministlikele ja hajussüsteemidele (1.01.2008−31.12.2011)", Jüri Vain, Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
ETF7667
Mudeli-põhine plaanurite süntees mittedeterministlikele ja hajussüsteemidele
Synthesis of model based reactive planners for nondeterministic and distributed systems
1.01.2008
31.12.2011
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
PerioodSumma
01.01.2008−31.12.2008238 800,00 EEK (15 262,10 EUR)
01.01.2009−31.12.2009229 248,00 EEK (14 651,62 EUR)
01.01.2010−31.12.2010208 386,00 EEK (13 318,29 EUR)
01.01.2011−31.12.201113 318,80 EUR
56 550,81 EUR

Taotluse teaduslik eesmärk on välja töötada reaktiivse plaanuri sünteesi meetod, mis põhineb kaasaegsetel kitsendustega programmeerimise ja esimest järku loogika tõestusmeetoditel. Valitud lähenemise üheks lähtehüpoteesiks on asjaolu, et paljud piisavalt kõrge abstraktsuse tasemega kirjeldatud planeerimisvaldkonnad saab esitada propositsionaalses keeles. Niisugune planeerimine eeldab sageli otsingut väga suures abstraktse plaani olekuruumis. Otsingu kiirendamiseks on kavas kasutada kehtestatavuse kontrollimise algoritme, mis on realiseeritud esimest järku teoreemitõestajas Gandalf, ja Bloomi filtritel põhinevat iteratiivse otsingu täpsustuse meetodit. Abstraktse plaani viimiseks täidetavale kujule, milleks on laiendatud lõpliku automaadi vorming, kasutame esimest järku loogika programmeerimise ja otsustustehnikaid. Sünteesitud reaktiivne plaanur peab toime tulema interaktiivse keskkonnaga, ebatäpse infoga keskkonna kohta ja planeerimise hajutatus paljude agentide vahel. Reaktiivse plaanuri sünteesimise meetod leiab edaspidi konkreetset kasutust hajusplaneerimisel robotiparvedes, mitte-deterministlike süsteemide mudelipõhisel testimisel ja kirurgi abi-roboti manipulaatori liikumise planeerimisel.
The research goal is to develop a synthesis method for reactive planners that is based on the state-of-the-art constraint programming and first-order logic based planning research. The approach will be built upon the hypothesis that at a high enough level of abstraction, many planning domains are essentially propositional. To search candidate abstract plans, large state spaces have to be searched. We use algorithms based on satisfiability testing implemented in the first order theorem prover Gandalf and methods stemming from the Bloom filters based iterated search refinement method. We use the logic programming and decision-theoretic techniques to expand the abstract plans to executable specifications formulated in terms of extended finite state machines. The synthesized planners have to cope with interactive environments, imprecise data about the environment and distribution of knowledge of between several agents. The method of reactive planner synthesis will be used in concrete applications: in the robot swarm planning, for model based testing of nondeterministic systems, and in scrub nurse robot motion planning