Hyper-Labeled Transition System and Its Application to Planning Under Linear Temporal Logic Constraints

Recently, formal methods have been paid much attention to in planning. We often leverage a labeled transition system (LTS) with a set of atomic propositions as a model of an environment. However, for example, in a flexible manufacturing system where an assembling machine has several functions that are performed exclusively, we need several states labeled by different sets of atomic propositions to discriminate the functions explicitly. This letter aims to reduce the number of the states. We introduce an extension of the LTS, called a
hyperLTS
, the labeling function of which assigns a set of sets of atomic propositions to each state. Then, we propose linear encodings for the hyperLTS to represent a sequence of pairs of a state and a selected set of atomic propositions. The hyperLTS-based modeling is consequently applied to a planning problem with one hard constraint and several soft constraints, thereby converting it into an integer linear programming problem. The effectiveness of the proposed modeling is illustrated through an example of a path planning problem of a mobile robot in a manufacturing system.