Directed Specifications and Assumption Mining for Monotone Dynamical Systems

Eric S. Kim, Murat Arcak, and Sanjit A. Seshia. Directed Specifications and Assumption Mining for Monotone Dynamical Systems. In Proceedings of the 9th International Conference on Hybrid Systems: Computation and Control (HSCC), April 2016.

Download

[pdf] 

Abstract

Given a dynamical system and a specification, assumption mining is the problem of identifying the set of admissible disturbance signals and initial states that generate trajectories satisfying the specification. We first introduce the notion of a directed specification, which describes either upper or lower sets in a partially ordered signal space, and show that this notion encompasses an expressive temporal logic fragment. We next show that the order preserving nature of monotone dynamical systems makes them amenable to a systematic form of assumption mining that checks numerical simulations of system trajectories against directed specifications. The assumption set is then located with a multidimensional bisection method that converges to the boundary from above and below. Typical objectives in vehicular traffic control, such as avoiding or clearing congestion, are directed specifications. In an application to a freeway flow model with monotone dynamics, we identify the set of vehicular demand profiles that satisfy a specification that congestion be intermittent.

BibTeX

@inproceedings{kim-hscc16,
  author    = {Eric S. Kim and Murat Arcak and Sanjit A. Seshia},
  title     = {Directed Specifications and Assumption Mining for Monotone Dynamical Systems},
 booktitle = {Proceedings of the 9th International Conference on Hybrid Systems: Computation and Control (HSCC)},
 month = "April",
 year = {2016},
 OPTpages = {239--248},
 abstract = {Given a dynamical system and a specification, assumption 
mining is the problem of identifying the set of admissible 
disturbance signals and initial states that generate  
trajectories satisfying the specification. We first introduce the 
notion of a directed specification, which describes either upper 
or lower sets in a partially ordered signal space, and show 
that this notion encompasses an expressive temporal logic 
fragment. We next show that the order preserving nature 
of monotone dynamical systems makes them amenable to a 
systematic form of assumption mining that checks numerical 
simulations of system trajectories against directed 
specifications. The assumption set is then located with a 
multidimensional bisection method that converges to the boundary 
from above and below. Typical objectives in vehicular traffic 
control, such as avoiding or clearing congestion, are directed 
specifications. In an application to a freeway flow model 
with monotone dynamics, we identify the set of vehicular 
demand profiles that satisfy a specification that congestion 
be intermittent.},
}