Differentiable Ternary Temporal Logic Semantics with Polynomial Surrogate Networks

Ryan Matheu; Sai Sandeep Damera; John S. Baras; Calin Belta

eess.SYOct 3, 2026

Differentiable Ternary Temporal Logic Semantics with Polynomial Surrogate Networks

Authors: Ryan Matheu, Sai Sandeep Damera, John S. Baras, Calin Belta

Organizations: Institute for Systems Research, University of Maryland, College Park, USA

Abstract

Temporal logic provides designers a formal reasoning tool for specifying complex spatio-temporal behaviors and tasks for autonomous systems. Many techniques exist for control synthesis according to temporal logic specifications, spanning a large variety of systems, including robotics. However, the vast majority of implementations are limited to Boolean temporal logics. Boolean temporal logic does not have an innate mechanism for quantifying abstention, rather verdicts are either definitively True or False. Recent work demonstrates that ternary logic is a capable formalism for reasoning about robotic behaviors, with the natural ability to classify uncertainty with the Unknown literal. Ternary temporal logic is still in its infancy, with work limited to synthesis for linear systems and monitoring. This work proposes a probabilistic relaxation of ternary temporal logic that allows for value and gradient computation through the same network while retaining exact verdicts on actual data. The relaxed network can be used as an objective in gradient-based control synthesis for both offline and online robotic control applications. We demonstrate the utility of our framework with two robotic manipulator tasks, one offline and one online, involving intermediate checking and sequencing of subtasks to demonstrate the benefit of our approach in terms of correct and timely execution.

Figures & tables

Panel of Figure 1 — Fig. 1: Ternary temporal logic-equivalent logic gate network for $\varphi=\seq(\lozenge_{[0,1]}\mu_{1},\,\square_{[0,1]}\mu_{2})$ at partial horizon $t_{2}=2$ . Each predicate is relaxed into a random trit, and its first two moments $(m,\,q)$ are propagated through the AND and OR gates in closed form, giving the distribution of the verdict $Z^{\varphi}_{0,2}$ . Search windows that extend beyond the partial horizon contribute constant Unknown inputs. The likelihood of satisfaction provides a smooth objective for gradient-based control synthesis.

Fig. 2: Example mean (left) and second moment (right) of a random predicate trit

Z^{\mu}

as functions of the value

f(x_{t})

for various noise scales

\tau

Open loop ( $N=140$ )
$\seq(\mathrm{Pre},\mathrm{Reach},\mathrm{Close},\mathrm{Lift},\sel(\mathrm{inspected},\mathrm{Scan}),\mathrm{Drop})\wedge\mathrm{Safe}$
Closed loop ( $H=50$ )
$\seq(\mathrm{Pre},\mathrm{Reach},\mathrm{Close},\sel(\mathrm{Place}_{A},\mathrm{Place}_{B}))\wedge\mathrm{Safe}$
Stage	Condition	Open-Loop	Closed-Loop
Pre	above part, gripper open	✓	✓
Reach	at part, gripper open	✓	✓

TABLE I: Bin-picking specifications.

Fig. 3: Open-loop plan for the uninspected cube with satisfaction likelihood $\Pr\bigl(Z^{\varphi}_{0,\,N}={+}1\bigr)=0.9998$ . The tool path is shown in red.

Fig. 4: Log-likelihood (top) that each sequential subtask has been completed by the open-loop controller at time

t

along the plan of Fig. 3 . Joint torques (bottom) normalized by their maximum value. Each joint torque command remains within its respective limits.

Fig. 5: Rollout snapshots for the closed-loop controller. Presence of a human causes the manipulator to fall back and place the item into the secondary bin. The task specification is achieved with likelihood of satisfaction $\Pr\bigl(Z^{\varphi_{\text{task}}}_{0,\,N}={+}1\bigr)=0.9999$ and safety non-violation $\Pr\bigl(Z^{\varphi_{\text{safe}}}_{0,\,N}\neq{-}1\bigr)=0.7996$ .

Fig. 6: Log-likelihood for the actual realized rollout and the predicted inner-loop with respect to time. When a coworker reaches for bin

A

, the bin-

A

candidate’s cost rises above bin

B

’s and the manipulator switches to placing the item in bin

B

, resulting in satisfaction of the specification.

	Open-loop : pick, inspect, and sort ( $N=100$ )	Closed-loop : conveyor pick with a moving hand ( $H=50$ , $N=160$ )
Pre	$\lozenge_{[0,N]}\square_{[0,2]}(\mathrm{at}(c_{\mathrm{pre}},0.03)\wedge\mathrm{open}\wedge\mathrm{aligned})$	$\lozenge_{[0,120]}\square_{[0,2]}(\mathrm{at}(c_{\mathrm{part}}{+}0.1e_{z},0.03)\wedge\mathrm{open}\wedge\mathrm{aligned})$
Reach	$\lozenge_{[0,N]}\square_{[0,2]}(\mathrm{at}(c_{\mathrm{grasp}},0.025)\wedge\mathrm{open}\wedge\mathrm{aligned})$	$\lozenge_{[0,30]}\square_{[0,2]}(\mathrm{at}(c_{\mathrm{grasp}},0.025)\wedge\mathrm{open}\wedge\mathrm{aligned}\wedge\mathrm{belt})$
Close	$\lozenge_{[0,N]}\square_{[0,6]}(\mathrm{at}(c_{\mathrm{grasp}},0.025)\wedge\mathrm{closed}\wedge\mathrm{aligned})$	$\lozenge_{[0,20]}\square_{[0,6]}(\mathrm{at}(c_{\mathrm{grasp}},0.025)\wedge\mathrm{closed}\wedge\mathrm{aligned}\wedge\mathrm{belt})$
Lift	$\lozenge_{[0,N]}\square_{[0,2]}(\mathrm{at}(c_{\mathrm{pre}},0.03)\wedge\mathrm{closed})$	–
Inspect	$\sel\bigl(\mathrm{inspected},\,\lozenge_{[0,N]}\square_{[0,10]}(\mathrm{at}(c_{\mathrm{scan}},0.04)\wedge\mathrm{facing})\bigr)$	–
Place	$\lozenge_{[0,N]}\square_{[0,6]}(\mathrm{at}(c_{\mathrm{drop}},0.04)\wedge\mathrm{open}\wedge\mathrm{still})$	$\sel(P_{A},P_{B})$ , $P_{A}=\seq\bigl(\lozenge_{[0,60]}\square_{[0,1]}(\mathrm{at}(c_{A},0.03)\wedge\mathrm{hold}\wedge\mathrm{free}_{A}),$

TABLE II: Case study specifications. Time bounds are in steps of

\delta t=0.05

s, and all predicates use

\delta=0.01

. The optimizer uses

\delta_{\mathrm{opt}}=0.015

and, in the closed-loop experiment, every

\square

window lengthened by 3 steps. Verdicts are certified on the specifications as listed.

Problem
	Open-loop : pick, scan, and sort	Closed-loop : conveyor pick, receding horizon
Robot	UFactory xArm7 with gripper (MJX), torque control
State, input	$x=(q,\dot{q},g)\in\mathbb{R}^{15}$ , $\|\dot{q}_{i}\|\leq 2$ rad/s; $u=(\tau,u_{g})\in\mathbb{R}^{8}$ , $\|\tau_{i}\|\leq\bar{\tau}_{i}$ , $\bar{\tau}=(50,50,30,30,30,20,20)$ Nm
Dynamics	MJX, contact-free, smoothed Coulomb friction; $\delta t=50$ ms
Specification	$\seq$ of 6 stages with $\sel(\mathrm{inspected},\mathrm{Scan})$	$\seq$ of 4 stages with $\sel(\mathrm{Place}_{A},\mathrm{Place}_{B})$ , deadline 6 s
AST nodes / predicates	60 / 17	82 / 23 (Task 58 / 12, Safe 24 / 11)

TABLE III: Detailed simulation parameters and results. Verdicts are exact

K_{3}

evaluations, probabilities are the smooth semantics with nominal

\delta=0.01

. Both experiments ran on NVIDIA RTX 5090 GPU, Intel Core Ultra 9 285K CPU.

Robotic Control

Robotic control studies how machines use sensing and computation to produce reliable movement and interaction in changing environments.

See all 562 papers

Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis
Apr 13, 2026Ryan Matheu, John S. Baras, Calin BeltaBehavior Trees Signal Temporal Logic
Institute for Systems Research, University of Maryland, College Park, USA.
Temporal logics and formal synthesis for robot planning and control
Jun 19, 2026Jana Tumova, Joris Verhagen, Matti VahsRobotic Control Signal Temporal Logic
KTH Royal Institute of Technology
Composing Learned Robot Behaviors with Temporal Logic at Runtime
Aug 13, 2026Moritz Zoellner, Anastasios Manganaris, Ahmed H. Qureshi +1Robot Task Planning Robot Policy Learning
Department of Computer Science, Purdue University

Apr 13, 2026J/K move · Enter open · S save

Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

Ryan Matheu, John S. Baras, Calin Belta

Institute for Systems Research, University of Maryland, College Park, USA.

Behavior Trees Signal Temporal Logic

Open paper AskPDF arXiv

Behavior Trees (BTs) provide designers with an intuitive graphical interface to construct long-horizon plans for autonomous systems. To ensure their correctness and safety, rigorous formal models and verification techniques are essential. Temporal BTs (TBTs) offer a promising approach by leveraging existing temporal logic formalisms to specify and verify the executions of BTs. However, this analysis is currently limited to offline post hoc analysis and trace repair. In this paper, we reformulate TBTs using a ternary-valued Signal Temporal Logic (STL) amenable to control synthesis. Ternary logic introduces a third truth value Unknown, formally capturing cases where a trajectory has neither fully satisfied nor violated a specification. We propose mixed-integer linear encodings for partial trajectory STL and TBTs over ternary logic, allowing for correct-by-construction control strategies for linear dynamical systems via mixed-integer optimization. We demonstrate the utility of our framework by solving optimal control problems.

Abstract

Robotic Control

Explore similar work

Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis

Temporal logics and formal synthesis for robot planning and control

Composing Learned Robot Behaviors with Temporal Logic at Runtime