2018 · 51 citations · 23 references
Mathematical ProgrammingDomain SpecificationEngineeringReachability ProblemComputational ComplexityFormal VerificationStrong Cyclic PlansSystems EngineeringTemporal LogicDigital PlanningMechanism DesignMulti-agent PlanningComputer ScienceFinite-state SystemPlanning TheoryAi PlanningAutomated ReasoningFond PlanningAutomationFormal MethodsObservable DomainsAutomaton Operation
We study planning for LTLf and LDLf temporally extended goals in nondeterministic fully observable domains (FOND). We consider both strong and strong cyclic plans, and develop foundational automata-based techniques to deal with both cases. Using these techniques we provide the computational characterization of both problems, separating the complexity in the size of the domain specification from that in the size of the formula. Specifically we establish them to be EXPTIME-complete and 2EXPTIME-complete, respectively, for both problems. In doing so, we also show 2EXPTIME-hardness for strong cyclic plans, which was open.
23
Finite Automata and Their Decision Problems
M. O. Rabin, D. Scott · IBM Journal of Research and Development · 1959 · 1.9K citations
On the synthesis of a reactive module
Amir Pnueli, Roni Rosner · 1989 · 1.4K citations · Full text