# TcCS-MF: Time Constrained Controller Synthesis for Multi-Affine Systems

**Description**

We consider the problem of controlling a multi-affine system such that its trajectories satisfy a temporal logic formula in a given amount of time.

We focus on specifications given as syntactically co-safe linear temporal logic formulas over rectangular regions in the state space.

To solve the main problem, we propose an algorithm based on estimating the time bounds for facet reachability problems and solving a time optimal reachability problem on the product between a weighted transition system and an automaton that enforces the satisfaction of the specification. Then, we use a random optimization algorithm to iteratively improve the solution.

The results of our work was published in ADHS 2012.

The tool TcCS-MF implements our solution. The tool is implemented in MATLAB and takes as input an automata file for specification, a set of rectangles and corresponding observations, and the dynamics of a multi-affine system.

- The FSA is constructed from the specification formula by using the tool scheck. A newer version of scheck is used for computation. The version is updated by Dr. Amit Bhatia and included in the package provided.
- The FSA file is converted to graph format for TcCS-MF. The tool lbt2dot is used for automata to graph translation, which also used for visualization.
- The random optimization toolbox PSOt implemented by Brian Birge is used to improve the solution.