The generation of route descriptions is a fundamental task of navigation systems. A particular problem in this context is to identify routes that can easily be described and processed by users. In this work, we present a framework for representing route networks with the qualitative information necessary to evaluate and optimize route descriptions with regard to ambiguities in them. We identify different agent models that differ in how agents are assumed to process route descriptions while navigating through route networks and (...) discuss which agent models can be translated into PDL programs. Further, we analyze the computational complexity of matching route descriptions and paths in route networks in dependency of the agent model. Finally, we empirically evaluate the influence of the agent model on the optimization and the processing of route instructions. (shrink)

Head-driven phrase structure grammar (HPSG) is one of the most prominent theories employed in deep parsing of natural language. Many linguistic theories are arguably best formalized in extensions of modal or dynamic logic (Keller, Feature logics, infinitary descriptions and grammar, 1993; Kracht, Linguistics Philos 18:401–458, 1995; Moss and Tiede, In: Blackburn, van Benthem, and Wolther (eds.) Handbook of modal logic, 2006), and HPSG seems to be no exception. Adequate extensions of dynamic logic have not been studied in detail, however; the (...) most important aspect is the reference to sets of substructures. In this paper, an adequate extension is identified, and some important results are established: Satisfiability is highly undecidable, and model checking is shown to be in EXPTIME and PSPACE-hard. A fragment with polynomial time model checking procedures is identified; it is shown to cover considerable fragments of HPSG. (shrink)

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically (...) for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2EXPTIME. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines. (shrink)

Formal learning theory is the mathematical embodiment of a normative epistemology. It deals with the question of how an agent should use observations about her environment to arrive at correct and informative conclusions. Philosophers such as Putnam, Glymour and Kelly have developed learning theory as a normative framework for scientific reasoning and inductive inference.