This paper introduces a way to plan long-running behaviors for robots and other systems so they both meet a logical task and visit a particular sequence of conditions with a desired long-run frequency. The authors call that frequency the long-run visit proportion. In plain terms, the method finds a repeating plan that makes a chosen pattern of conditions appear a given fraction of the time in the repeating part of the plan.

The researchers formalize the problem and give a synthesis method. They model the system as a finite, deterministic weighted transition system — that is, a set of regions or states, allowed moves with costs, and labels that say which conditions hold at each state. High-level tasks are written in linear temporal logic (LTL), a way to say things like “eventually visit A” or “always avoid B” over an infinite execution. The paper defines the long-run visit proportion for a path written in prefix–suffix form (a one-time prefix followed by a repeating suffix) and then finds prefix–suffix paths that satisfy the LTL task, respect an overall cost limit, and keep the long-run visit proportion close to a desired target within a given tolerance.

At a high level the synthesis uses automata-based ideas common in LTL planning. The method searches for a prefix and a cyclic suffix whose repeated trace gives the right asymptotic frequency of a specified finite sequence of atomic propositions (an atomic proposition is simply a basic true/false condition at a region). By changing the desired proportion, the planner can make the repeating behavior spend more or less attention on the sequence of interest, while also observing a cost budget.

This matters because standard LTL is qualitative: it can require that something happens or happens infinitely often, but it cannot directly ask that a particular finite sequence occurs a specified fraction of the time. Other formalisms have addressed related ideas — for example, logics that compare multiple executions or steady-state visit constraints on single states — but they do not directly express the asymptotic proportion of a specific ordered sequence inside a repeating trace. The authors also show experiments on a quadruped robot to illustrate that the notion and planner can be used in practice.