Hierarchical Planning through Propositional Logic – Highly Efficient, Versatile, and Flexible. Behnke, G. Ph.D. Thesis, Ulm University, 2019. ![Hierarchical Planning through Propositional Logic – Highly Efficient, Versatile, and Flexible [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Dissertation doi abstract bibtex AI Planning is a core technology in enabling advanced assistance for human users. When faced with complex problems such as handicraft tasks for household repairs, Do-It-Yourself projects, or difficult assembly tasks, a planning-based assistance system can provide individualised and context-dependent instructions. It thus effectively supports the user in achieving his or her goals. High-quality assistance should in addition conform to the user’s current wishes and preferences to ensure maximum utility. This can be achieved by involving the user into the planning process, i.e. by making planning mixed-initiative. Hierarchical Task Network (HTN) planning is a method particularly well suited for providing user support, as it resembles the means and structures humans use for problem solving. We identified two major challenges that every mixed-initiative HTN planning system must face and show how to address them: generating plans quickly and flexibly altering them according to the user’s demands.
The main focus of this thesis lies on addressing the first challenge, i.e. on developing a quickly responding and efficient HTN planner. Designing efficient HTN planners is particularly difficult. Their algorithms have to take both dimensions of the problem description – state and hierarchy – into account and have to consider interactions between them. We use a translation into propositional logic, enabling for the first time a uniform view on the whole planning problem. First, we describe a new encoding for totally-ordered HTN planning, before extending it in two consecutive steps to capture general, partially-ordered domains. Second, we introduce Path Decomposition Trees (PDTs) and Solution Order Graphs (SOGs) which enable a compact encoding and alleviate unnecessary reasoning from a SAT solver. They also pave the way for future insights into structural properties of HTN planning problems, which allow for more efficient planning as well as for more advanced user support. Third, we show that our encodings are a significant empirical improvement over the current state of the art in HTN planning. Lastly, we present a fundamental technique for optimal HTN planning – which is especially important in assistance scenarios – namely a method to compute succinct depth bounds for plan-length optimisation.
In a mixed-initiative planning environment, users will frequently request the planner to change a currently considered plan. We start solving this second challenge by considering the most basic task involved: to verify that the changed plan is a solution to the planning problem at hand. First, we show that this task is NP-complete. Second, we develop the first plan verifier for HTN planning, which is based on a transformation into propositional logic. Third, we analyse and categorise the requests possibly made by a user and show that the objectives posed by her or him can be suitably represented as formulae in Linear Temporal Logic (LTL). Fourth, we analyse the computational complexity of changing a plan, showing that this task can be between NP-complete and undecidable. Lastly, we use our SAT-based planner to change a plan with respect to a request formulated as an LTL formula. We show that the full spectrum of LTL formulae can be supported efficiently in a propositional encoding. For that, we introduce a new theoretical foundation for reasoning about parallelism in LTL traces.
The practical applicability of our techniques has been demonstrated within a joint transfer project with Robert Bosch GmbH. In it, we developed an assistance system that guides novice users through a handicraft Do-It-Yourself project. The underlying hierarchical planning model is highly complex. Currently the only planner that is able to find plans for this model within an acceptable time frame is the SAT-based HTN planner developed as part of this thesis.
@PhdThesis{Behnke2019PhDThesis,
author = {Gregor Behnke},
title = {Hierarchical Planning through Propositional Logic -- Highly Efficient, Versatile, and Flexible},
school = {Ulm University},
year = {2019},
abstract = {AI Planning is a core technology in enabling advanced assistance for human users. When faced with complex problems such as handicraft tasks for household repairs, Do-It-Yourself projects, or difficult assembly tasks, a planning-based assistance system can provide individualised and context-dependent instructions. It thus effectively supports the user in achieving his or her goals. High-quality assistance should in addition conform to the user’s current wishes and preferences to ensure maximum utility. This can be achieved by involving the user into the planning process, i.e. by making planning mixed-initiative. Hierarchical Task Network (HTN) planning is a method particularly well suited for providing user support, as it resembles the means and structures humans use for problem solving. We identified two major challenges that every mixed-initiative HTN planning system must face and show how to address them: generating plans quickly and flexibly altering them according to the user’s demands.<br/><br/>
The main focus of this thesis lies on addressing the first challenge, i.e. on developing a quickly responding and efficient HTN planner. Designing efficient HTN planners is particularly difficult. Their algorithms have to take both dimensions of the problem description – state and hierarchy -- into account and have to consider interactions between them. We use a translation into propositional logic, enabling for the first time a uniform view on the whole planning problem. First, we describe a new encoding for totally-ordered HTN planning, before extending it in two consecutive steps to capture general, partially-ordered domains. Second, we introduce Path Decomposition Trees (PDTs) and Solution Order Graphs (SOGs) which enable a compact encoding and alleviate unnecessary reasoning from a SAT solver. They also pave the way for future insights into structural properties of HTN planning problems, which allow for more efficient planning as well as for more advanced user support. Third, we show that our encodings are a significant empirical improvement over the current state of the art in HTN planning. Lastly, we present a fundamental technique for optimal HTN planning -- which is especially important in assistance scenarios – namely a method to compute succinct depth bounds for plan-length optimisation.<br/><br/>
In a mixed-initiative planning environment, users will frequently request the planner to change a currently considered plan. We start solving this second challenge by considering the most basic task involved: to verify that the changed plan is a solution to the planning problem at hand. First, we show that this task is NP-complete. Second, we develop the first plan verifier for HTN planning, which is based on a transformation into propositional logic. Third, we analyse and categorise the requests possibly made by a user and show that the objectives posed by her or him can be suitably represented as formulae in Linear Temporal Logic (LTL). Fourth, we analyse the computational complexity of changing a plan, showing that this task can be between NP-complete and undecidable. Lastly, we use our SAT-based planner to change a plan with respect to a request formulated as an LTL formula. We show that the full spectrum of LTL formulae can be supported efficiently in a propositional encoding. For that, we introduce a new theoretical foundation for reasoning about parallelism in LTL traces.<br/><br/>
The practical applicability of our techniques has been demonstrated within a joint transfer project with Robert Bosch GmbH. In it, we developed an assistance system that guides novice users through a handicraft Do-It-Yourself project. The underlying hierarchical planning model is highly complex. Currently the only planner that is able to find plans for this model within an acceptable time frame is the SAT-based HTN planner developed as part of this thesis.},
doi = {10.18725/OPARU-23396},
url_Dissertation = {https://oparu.uni-ulm.de/xmlui/bitstream/handle/123456789/23459/thesis_behnke.pdf}
}
Downloads: 0
{"_id":"hkEDvKcjgwY9Y4wqS","bibbaseid":"behnke-hierarchicalplanningthroughpropositionallogichighlyefficientversatileandflexible-2019","authorIDs":[],"author_short":["Behnke, G."],"bibdata":{"bibtype":"phdthesis","type":"phdthesis","author":[{"firstnames":["Gregor"],"propositions":[],"lastnames":["Behnke"],"suffixes":[]}],"title":"Hierarchical Planning through Propositional Logic – Highly Efficient, Versatile, and Flexible","school":"Ulm University","year":"2019","abstract":"AI Planning is a core technology in enabling advanced assistance for human users. When faced with complex problems such as handicraft tasks for household repairs, Do-It-Yourself projects, or difficult assembly tasks, a planning-based assistance system can provide individualised and context-dependent instructions. It thus effectively supports the user in achieving his or her goals. High-quality assistance should in addition conform to the user’s current wishes and preferences to ensure maximum utility. This can be achieved by involving the user into the planning process, i.e. by making planning mixed-initiative. Hierarchical Task Network (HTN) planning is a method particularly well suited for providing user support, as it resembles the means and structures humans use for problem solving. We identified two major challenges that every mixed-initiative HTN planning system must face and show how to address them: generating plans quickly and flexibly altering them according to the user’s demands.<br/><br/> The main focus of this thesis lies on addressing the first challenge, i.e. on developing a quickly responding and efficient HTN planner. Designing efficient HTN planners is particularly difficult. Their algorithms have to take both dimensions of the problem description – state and hierarchy – into account and have to consider interactions between them. We use a translation into propositional logic, enabling for the first time a uniform view on the whole planning problem. First, we describe a new encoding for totally-ordered HTN planning, before extending it in two consecutive steps to capture general, partially-ordered domains. Second, we introduce Path Decomposition Trees (PDTs) and Solution Order Graphs (SOGs) which enable a compact encoding and alleviate unnecessary reasoning from a SAT solver. They also pave the way for future insights into structural properties of HTN planning problems, which allow for more efficient planning as well as for more advanced user support. Third, we show that our encodings are a significant empirical improvement over the current state of the art in HTN planning. Lastly, we present a fundamental technique for optimal HTN planning – which is especially important in assistance scenarios – namely a method to compute succinct depth bounds for plan-length optimisation.<br/><br/> In a mixed-initiative planning environment, users will frequently request the planner to change a currently considered plan. We start solving this second challenge by considering the most basic task involved: to verify that the changed plan is a solution to the planning problem at hand. First, we show that this task is NP-complete. Second, we develop the first plan verifier for HTN planning, which is based on a transformation into propositional logic. Third, we analyse and categorise the requests possibly made by a user and show that the objectives posed by her or him can be suitably represented as formulae in Linear Temporal Logic (LTL). Fourth, we analyse the computational complexity of changing a plan, showing that this task can be between NP-complete and undecidable. Lastly, we use our SAT-based planner to change a plan with respect to a request formulated as an LTL formula. We show that the full spectrum of LTL formulae can be supported efficiently in a propositional encoding. For that, we introduce a new theoretical foundation for reasoning about parallelism in LTL traces.<br/><br/> The practical applicability of our techniques has been demonstrated within a joint transfer project with Robert Bosch GmbH. In it, we developed an assistance system that guides novice users through a handicraft Do-It-Yourself project. The underlying hierarchical planning model is highly complex. Currently the only planner that is able to find plans for this model within an acceptable time frame is the SAT-based HTN planner developed as part of this thesis.","doi":"10.18725/OPARU-23396","url_dissertation":"https://oparu.uni-ulm.de/xmlui/bitstream/handle/123456789/23459/thesis_behnke.pdf","bibtex":"@PhdThesis{Behnke2019PhDThesis,\n author = {Gregor Behnke},\n title = {Hierarchical Planning through Propositional Logic -- Highly Efficient, Versatile, and Flexible},\n school = {Ulm University},\n year = {2019},\n abstract = {AI Planning is a core technology in enabling advanced assistance for human users. When faced with complex problems such as handicraft tasks for household repairs, Do-It-Yourself projects, or difficult assembly tasks, a planning-based assistance system can provide individualised and context-dependent instructions. It thus effectively supports the user in achieving his or her goals. High-quality assistance should in addition conform to the user’s current wishes and preferences to ensure maximum utility. This can be achieved by involving the user into the planning process, i.e. by making planning mixed-initiative. Hierarchical Task Network (HTN) planning is a method particularly well suited for providing user support, as it resembles the means and structures humans use for problem solving. We identified two major challenges that every mixed-initiative HTN planning system must face and show how to address them: generating plans quickly and flexibly altering them according to the user’s demands.<br/><br/>\n\n The main focus of this thesis lies on addressing the first challenge, i.e. on developing a quickly responding and efficient HTN planner. Designing efficient HTN planners is particularly difficult. Their algorithms have to take both dimensions of the problem description – state and hierarchy -- into account and have to consider interactions between them. We use a translation into propositional logic, enabling for the first time a uniform view on the whole planning problem. First, we describe a new encoding for totally-ordered HTN planning, before extending it in two consecutive steps to capture general, partially-ordered domains. Second, we introduce Path Decomposition Trees (PDTs) and Solution Order Graphs (SOGs) which enable a compact encoding and alleviate unnecessary reasoning from a SAT solver. They also pave the way for future insights into structural properties of HTN planning problems, which allow for more efficient planning as well as for more advanced user support. Third, we show that our encodings are a significant empirical improvement over the current state of the art in HTN planning. Lastly, we present a fundamental technique for optimal HTN planning -- which is especially important in assistance scenarios – namely a method to compute succinct depth bounds for plan-length optimisation.<br/><br/>\n\n In a mixed-initiative planning environment, users will frequently request the planner to change a currently considered plan. We start solving this second challenge by considering the most basic task involved: to verify that the changed plan is a solution to the planning problem at hand. First, we show that this task is NP-complete. Second, we develop the first plan verifier for HTN planning, which is based on a transformation into propositional logic. Third, we analyse and categorise the requests possibly made by a user and show that the objectives posed by her or him can be suitably represented as formulae in Linear Temporal Logic (LTL). Fourth, we analyse the computational complexity of changing a plan, showing that this task can be between NP-complete and undecidable. Lastly, we use our SAT-based planner to change a plan with respect to a request formulated as an LTL formula. We show that the full spectrum of LTL formulae can be supported efficiently in a propositional encoding. For that, we introduce a new theoretical foundation for reasoning about parallelism in LTL traces.<br/><br/>\n\n The practical applicability of our techniques has been demonstrated within a joint transfer project with Robert Bosch GmbH. In it, we developed an assistance system that guides novice users through a handicraft Do-It-Yourself project. The underlying hierarchical planning model is highly complex. Currently the only planner that is able to find plans for this model within an acceptable time frame is the SAT-based HTN planner developed as part of this thesis.},\n doi = {10.18725/OPARU-23396},\n url_Dissertation = {https://oparu.uni-ulm.de/xmlui/bitstream/handle/123456789/23459/thesis_behnke.pdf}\n}\n\n\n","author_short":["Behnke, G."],"key":"Behnke2019PhDThesis","id":"Behnke2019PhDThesis","bibbaseid":"behnke-hierarchicalplanningthroughpropositionallogichighlyefficientversatileandflexible-2019","role":"author","urls":{" dissertation":"https://oparu.uni-ulm.de/xmlui/bitstream/handle/123456789/23459/thesis_behnke.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"phdthesis","biburl":"hierarchical-task.net/bibtex/theses-in-hierarchical-planning.bib","creationDate":"2020-04-25T03:46:49.123Z","downloads":5,"keywords":[],"search_terms":["hierarchical","planning","through","propositional","logic","highly","efficient","versatile","flexible","behnke"],"title":"Hierarchical Planning through Propositional Logic – Highly Efficient, Versatile, and Flexible","year":2019,"dataSources":["vY5emPje84NjvCwk9"]}