When Goals Collide: Synthesizing the Best Possible Outcome

A robot does not always get the luxury of a clean task list.

Reach the loading bay. Avoid blocked corridors. Preserve battery. Pick up two packages. Respect a safety boundary. Finish before the door closes. Then the environment, as environments enjoy doing, changes the rules halfway through. A corridor shuts. A resource disappears. One goal now interferes with another.

The usual synthesis question is brutally binary: can the agent guarantee the whole specification, yes or no? If yes, synthesize a controller. If no, declare failure and go home with the quiet dignity of a spreadsheet cell returning FALSE.

The paper Multi-Property Synthesis asks a better question: when the full specification cannot be guaranteed, which subsets of goals can still be guaranteed, and how do we synthesize a strategy for a best achievable subset?¹ That is not just a softer mood. It changes synthesis from a pass/fail oracle into a trade-off engine for finite-horizon agents.

The important word here is guaranteed. This is not a utility maximizer choosing what it happens to prefer. It is not a planner hoping the environment behaves. The paper stays inside the formal synthesis world: an agent must satisfy goals against all admissible environment behaviors. The contribution is to make that world less brittle when goals collide.

The old question fails exactly when real systems become interesting

Traditional LTLf synthesis works well when the specification is one coherent target. LTLf, or Linear Temporal Logic over finite traces, is useful for tasks that are meant to end: planning, service composition, business-process execution, finite-horizon robot behavior. The standard pipeline converts the temporal formula into an automaton, turns the automaton into a reachability game, and asks whether the agent has a strategy that forces the game into an accepting state.

That machinery is elegant because the objective is clear. Reach acceptance, then stop.

It is also unforgiving because real systems rarely arrive as one polite objective. They arrive as bundles:

The naive response is enumeration. For every subset of goals, build or solve a synthesis problem for the conjunction of that subset. If the system has $n$ goals, there are $2^n$ subsets. The algorithm is simple in the same way that testing every possible password is simple. Conceptually reassuring, operationally rude.

The paper’s mechanism-first move is to avoid asking the same question over and over. Instead of solving one synthesis instance per subset, it builds a single product game that tracks progress toward all goals at once.

The product game does not have one finish line

For each goal, the method constructs a deterministic finite automaton that accepts exactly the finite traces satisfying that goal. Then it forms a product arena across the goal automata. A product state records where the agent currently stands with respect to each goal.

In ordinary synthesis, the game has a designated accepting set. In multi-property synthesis, there is no single finish line. A state may satisfy goal 1 and goal 3 but not goal 2. Another state may satisfy goal 2 only. Another may satisfy all goals, the dream scenario before reality starts charging rent.

So the paper defines satisfaction relative to a goal set. A product state satisfies a set of goals if the automaton component for every goal in that set is accepting. From there, the core object becomes a relation:

This relation says: from this state, the agent can guarantee this goal set, no matter how the environment responds.

That sentence is doing the heavy lifting. It is not asking whether a state is simply winning or losing. It asks which collections of goals are winnable from each state. The answer becomes a map of achievable trade-offs.

The fixed point turns trade-offs into a computable relation

The paper’s central algorithm is a fixed-point computation over state–goal-set pairs.

The base case is local and intuitive. If the current product state already satisfies all goals in a set $G$, then $G$ is realizable from that state: the agent can stop immediately.

The inductive step mirrors standard controllable-predecessor reasoning. A goal set $G$ is realizable from a state if the agent has an output choice such that, for every possible environment input, the successor state still has $G$ as realizable.

Put less formally:

1. If you have already achieved the target goals, stop.
2. Otherwise, choose an action that keeps the target goals enforceable regardless of the environment’s next move.
3. Repeat until the fixed point stabilizes.

This is the same conceptual skeleton as ordinary reachability synthesis, but lifted from “which states are winning?” to “which goal sets are winning from which states?”

That lift matters because it preserves the adversarial guarantee. The method does not say, “This subset is likely.” It says, “This subset can be forced.” In business language, it is not a recommendation engine. It is a guarantee boundary.

Monotonicity is the compression trick hiding in plain sight

The first fixed-point relation can still be large. A state may be associated with many realizable subsets. But multi-property realizability has a useful monotonic structure:

If a system can guarantee goals ${A, B, C}$, then it can also guarantee ${A, B}$, ${A, C}$, ${B}$, and every other subset.

That sounds obvious. It is also the reason the method can avoid storing a great deal of redundant information.

The paper introduces a maximal variant that keeps only maximal realizable goal sets for each state. Smaller subsets remain implicit. If ${A, B, C}$ is realizable, there is no need to separately carry ${A, B}$ unless it matters as a different maximal branch elsewhere.

This is where the accepted editorial framing becomes important. The paper is not merely saying, “enumeration is slow.” Everyone already knows exponential enumeration is slow; congratulations, the calendar remains undefeated. The better point is that the search space has structure. The algorithm exploits the fact that achievement is downward closed.

The maximal-set variant does not magically destroy worst-case complexity. The paper is clear about that. The number of maximal subsets can still be exponential in the number of goals. But in practical symbolic synthesis, “not storing what is already implied” is often the difference between a tool and a decorative theorem.

The symbolic version is where the mechanism becomes practical

The symbolic synthesis section is the paper’s real leverage point.

Instead of explicitly listing goal sets, the method introduces Boolean variables for goals. A valuation over these variables represents a subset of goals. If the variable for goal $i$ is true, that goal is included in the claimed set.

The initial winning relation is encoded as a Boolean formula that says, in effect:

That implication is small, but it carries the monotonicity. If a formula satisfies a larger goal set, it automatically represents satisfaction of smaller subsets when corresponding goal variables are turned off. The symbolic representation therefore captures many goal combinations without listing them.

The paper emphasizes a pleasant technical fact: after adding goal variables, the symbolic multi-property algorithm is almost the same as the symbolic single-property algorithm. The same kind of fixed-point computation runs over state variables and goal variables together. The machinery does not require a strange custom operator for every subset. It simply lets Boolean structure carry the combinatorics.

For readers thinking about agentic systems, this is the durable lesson: the paper does not beat combinatorial explosion by pretending it is not there. It changes the representation so shared structure can be reused.

This is not preference planning wearing a formal-methods jacket

A likely misunderstanding is to read this as another form of preference planning: assign values to goals, optimize the score, and pick the best available plan.

That is not what the paper does.

Preference planning and over-subscription planning often ask which goals are most valuable under resource limits. Many such methods work in non-adversarial models or optimize a scalar utility. This paper instead computes which goal subsets are realizable under adversarial environment behavior. The result is qualitative and set-based, not utility-weighted.

The distinction matters.

The paper does mention future directions such as weighted properties, probabilistic environments, and online adaptation. Those are natural extensions. They are not already solved here. Good. A paper should not be punished for not being three papers in a trench coat.

The experiments mainly test shared computation against enumeration

The experiments evaluate a tool called MPSynth, built on symbolic synthesis infrastructure. The baseline enumerates subsets and checks realizability using single-property symbolic synthesis, with pruning: it explores subsets and avoids checking supersets once a subset is known to be unrealizable.

That is a fairer baseline than the dumbest possible enumeration. It still repeats too much work.

The benchmark families are designed to stress different parts of the mechanism:

The representative table reports substantial runtime gains. On the counter instance with 373,920 states, MPSynth takes 4.713 seconds while enumeration takes 60.74 seconds, roughly a 12.9× speedup. On the largest listed next instance, with 105,413,504 states, MPSynth takes 611.90 seconds against 4925.10 seconds for enumeration, roughly 8.0×. On the largest listed until instance, with 60,466,176 states, MPSynth takes 562.70 seconds against 2640.49 seconds, roughly 4.7×. On the largest robotnav instance, with 100,663,296 states, MPSynth takes 1003.21 seconds against 2812.53 seconds, roughly 2.8×.

The “up to two orders of magnitude” result appears most strongly on smaller or more favorable instances, such as the chain family. The more interesting lesson is not that every large case gets a hundredfold acceleration. It does not. The better lesson is that the method consistently avoids enumeration’s repeated synthesis work across very different benchmark structures.

The appendix also separates fixed-point computation from maximal-set and strategy extraction. The extraction step is usually tiny compared with fixed-point computation. That matters operationally: the bottleneck is computing the realizability relation, not selecting the final maximal goal set and extracting the corresponding controller.

So the experimental message should be read carefully. This is main evidence for computational efficiency against enumeration, with benchmark diversity giving some robustness. It is not an ablation proving which single design choice contributes how much. The paper does not, for example, separately isolate the marginal effect of maximal pruning versus symbolic goal variables across a controlled ablation table. The experiments support the combined method.

The business value is not “better optimization”; it is defensible degradation

For Cognaptus readers, the temptation is to translate this paper into a familiar phrase: graceful degradation. That is partly right, but too vague.

The sharper business interpretation is defensible degradation.

When an automated system cannot satisfy all objectives, it should not merely fail, improvise, or choose whatever looks locally convenient. It should be able to say:

• these goal combinations are enforceable;
• these are not enforceable under the modeled environment;
• this maximal set is selected;
• here is a strategy that guarantees it;
• here is where the guarantee stops.

That is valuable in any setting where automation touches obligations, not just preferences.

Consider workflow orchestration. A business process may include deadlines, approvals, notifications, audit trails, and exception handling. If all obligations cannot be met under a finite horizon, a synthesis system that only returns “unrealizable” is not very helpful. A multi-property system could identify the maximal enforceable subset and produce an execution strategy that satisfies it.

Consider service composition. Multiple services may have dependencies and failure modes. A controller may not guarantee all service-level objectives under every environment behavior, but it may guarantee a meaningful subset. Knowing that subset before deployment is better than discovering it through user complaints, also known as the traditional enterprise observability stack.

Consider robotics. A robot may face several spatial goals and constraints. The method’s robot-navigation benchmarks are not proof of field deployment, but they illustrate the right kind of structure: reaching one region can make another unreachable, while the environment can close parts of the world. A controller that knows the maximal guaranteed objectives is more useful than one that treats the full mission as simply dead.

What the paper directly shows, and what business readers may infer

It is useful to separate the paper’s contribution from the business interpretation, because otherwise every formal-methods paper somehow becomes a platform strategy. That way lies pitch-deck confetti.

The business value is strongest where objectives can be formalized as finite-horizon temporal properties and where guarantees matter more than approximate preference satisfaction. That includes safety-critical workflows, regulated process automation, robotic task planning, and certain kinds of agent orchestration.

The value is weaker where the environment is poorly specified, goals are vague, preferences dominate hard guarantees, or success is probabilistic rather than adversarial. In those settings, this paper may still inspire architecture, but it is not a drop-in solution.

The boundary: formal guarantees require formal inputs

The main practical limitation is not hidden in the math. It is sitting in front of anyone who has ever tried to formalize a business rule.

The method assumes goals are expressed as LTLf properties over atomic propositions. That is appropriate for finite tasks with clear temporal structure. It is less natural for fuzzy user satisfaction, open-ended conversation quality, or market-facing business objectives that shift every Tuesday because someone saw a competitor dashboard.

The method is also qualitative. It asks whether a set of goals can be guaranteed against all admissible environment behaviors. It does not assign probabilities to partial success. It does not rank goals by revenue value. It does not say that satisfying three minor goals is better than satisfying one mission-critical goal. The paper’s conclusion explicitly points toward weighted properties and probabilistic environments as future work.

Finally, the worst-case complexity remains 2EXPTIME-complete. The algorithm improves practical computation by sharing structure and using symbolic representation; it does not repeal complexity theory. Complexity theory, annoyingly, has tenure.

These boundaries do not weaken the contribution. They define where it should be used.

Why the mechanism matters for agentic systems

Modern agent discussions often focus on memory, tool use, reflection, and multi-agent communication. Those are important. But many agent failures are less cinematic: the system has too many goals, some conflict, and nobody knows what should happen when the conjunction breaks.

Multi-property synthesis offers a formal vocabulary for that situation. It says: do not treat failure as a binary event. Treat it as a structured frontier. Compute what can still be guaranteed. Extract the controller that achieves it. Leave preference weights and probabilistic adaptation for the layer that actually models them.

That framing is especially useful for enterprise AI because organizations rarely need agents that are merely “more autonomous.” They need agents whose limits can be inspected before autonomy becomes expensive.

The paper’s mechanism-first contribution is therefore simple to state and hard to implement well:

1. Build one product arena for all properties.
2. Compute the relation between states and realizable goal sets.
3. Use monotonicity to keep maximal sets and imply smaller ones.
4. Encode goal sets symbolically with Boolean variables.
5. Extract a maximal realizable set and a strategy that guarantees it.

That is the difference between an agent that says, “I cannot do everything,” and an agent architecture that can answer, “Here is the best enforceable outcome, and here is the proof-shaped reason.”

Conclusion: the useful answer is not always yes

The paper’s real contribution is not that it makes synthesis faster, although it often does. It is that it asks a more operational question.

In constrained finite-horizon systems, “Can I satisfy the full specification?” is often the least interesting question because the answer may be no. The useful question is what remains possible after no.

Multi-property synthesis gives that question a formal shape. It computes the achievable frontier, keeps maximal goal sets explicit, uses symbolic structure to avoid brute-force enumeration, and synthesizes strategies rather than merely issuing diagnoses.

For business automation, that points toward a healthier design principle: when goals collide, do not let the system improvise quietly. Make the trade-off frontier explicit before deployment. Then choose the best enforceable outcome with eyes open.

A little less magical autonomy. A little more accountable machinery. Tragic for the hype cycle, useful for everyone else.

Cognaptus: Automate the Present, Incubate the Future.