  The control of dynamical systems under temporal logic specifications among
uncontrollable dynamic agents is challenging due to the agents' a-priori
unknown behavior. Existing works have considered the problem where either all
agents are controllable, the agent models are deterministic and known, or no
safety guarantees are provided. We propose a predictive control synthesis
framework that guarantees, with high probability, the satisfaction of signal
temporal logic (STL) tasks that are defined over the system and uncontrollable
stochastic agents. We use trajectory predictors and conformal prediction to
construct probabilistic prediction regions for each uncontrollable agent that
are valid over multiple future time steps. Specifically, we reduce conservatism
and increase data efficiency compared to existing works by constructing a
normalized prediction region over all agents and time steps. We then formulate
a worst-case mixed integer program (MIP) that accounts for all agent
realizations within the prediction region to obtain control inputs that
provably guarantee task satisfaction with high probability. To efficiently
solve this MIP, we propose an equivalent MIP program based on KKT conditions of
the original one. We illustrate our control synthesis framework on two case
studies.
