Control Synthesis for Parametric Timed Automata under Unavoidability Specifications

TL;DR

This paper presents a novel algorithm for control synthesis and parameter valuation in parametric timed automata to ensure timely reachability of target states while avoiding unsafe locations, demonstrated through a robotic planning example.

Contribution

It introduces an iterative depth-first analysis algorithm combined with feasibility checks and MILP solving for control and parameter synthesis in PTAs.

Findings

Successfully synthesizes control strategies for PTAs

Ensures reachability within time bounds while avoiding unsafe states

Demonstrated effectiveness on a robotic planning example

Abstract

Timed automata (TA) is used for modeling systems with timing aspects. A TA extends a finite automaton with a set of real valued variables called clocks, that measure the time and constraints over the clocks guard the transitions. A parametric TA (PTA) is a TA extension that allows parameters in clock constraints. In this paper, we focus on synthesis of a control strategy and parameter valuation for a PTA such that each run of the resulting TA reaches a target location within the given amount of time while avoiding unsafe locations. We propose an algorithm based on depth first analysis combined with an iterative feasibility check. The algorithm iteratively constructs a symbolic representation of the possible solutions, and employs a feasibility check to terminate the exploration along infeasible directions. Once the construction is completed, a mixed integer linear program is solved for each candidate strategy to generate a parameter valuation and a control strategy pair. We present a robotic planning example to motivate the problem and to illustrate the results.