Hybrid  dynamical systems, coupled with sensor networks have had tremendous impacts on every aspects of our daily lives. Concerns of safety, reliability,  and efficiency demands researchers to develop new tools and technologies to help analyze such systems. Unfortunately, there is a paucity of standard benchmark systems and accompanying requirements that researchers can use to evaluate and compare the efficacy of their techniques. A closed-loop model of an industrial control system typically involves a plant model describing the dynamical characteristics of the physical processes within the system, and a controller model, which is usually a block-diagram-based representation of the software used to regulate the plant behavior.

In practice, industrial-scale plant models and controller models are very complex as they can contain highly nonlinear hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, and so on. Moreover, the de facto standard in the automotive and avionics domains is to describe such models in the modeling language Simulink(r). As the formal semantics of Simulink are not public, it makes formal analysis challenging.

In this talk, we will present a suite of closed-loop models of powertrain control systems from the automotive domain. These benchmarks are intended to challenge the research community while maintaining a manageable scale.  As local requirements amenable to use with verification tools are not typically available, we also present a set of representative requirements specifying the quality of the closed-loop control system.


Xiaoqing Jin is a senior engineer and researcher at Toyota Technical Center in Gardena (Los Angeles) California. Her research interests are in the broad area of formal verification, automatic synthesis and repair of systems, and temporal logic.  Her current focus is in the area of cyber-physical systems, in particular, automotive control systems modeled as hybrid automata and nonlinear dynamical systems. Previously, Xiaoqing got her PhD in the area of formal verification and validation for  hybrid systems under the supervision of  Gianfranco Ciardo (who is currently at Iowa State University) at the University of California, Riverside.

Several types of automata, such as probabilistic and quantum automata, require to work with real and complex numbers. For such automata the acceptance of an input is quantified with a probability. There are plenty of results in the literature addressing the complexity of checking the equivalence of these automata, that is, checking whether two automata accept all inputs with the same probability. On the other hand, the critical problem of finding the minimal automata equivalent to a given one has been left open (C. Moore, J.P. Crutchfield, Theoretical Computer Science 237 (2000) 275-306, p. 304, Problem 5).

In this work, we reduce the minimization problem of probabilistic and quantum automata to finding a solution of a system of algebraic polynomial (in)equations. An EXPSPACE upper bound on the complexity of the minimization problem is derived by applying Renegar's algorithm. More specifically, we show that the state minimization of probabilistic automata, measure-once quantum automata, measure-many quantum automata, measure-once generalized quantum automata, and measure-many generalized quantum automata is decidable and in EXPSPACE. Finally, we also solve an open problem concerning minimal covering of stochastic sequential machines (A. Paz, Introduction to Probabilistic Automata, Academic Press, 1971, Page 43). Joint work with D. Qiu and L. Li published in Information and Computation.


Born in 1975 in Lisbon, Paulo Mateus studied at IST where he got his PhD in 2001 with a thesis on the interconnection of probabilistic systems. In the Fall semester of 2001-02, he was a postdoc at the Logic and Computation Group, Department of Mathematics, University of Pennsylvania. In 2006, he obtained his agregação (habilitation) in Mathematics from the Technical University of Lisbon. His habilitation thesis was awarded the Portuguese IBM Scientific Prize 2005. Currently, he is an Associate Professor at the Department of Mathematics of IST and coordinates the Security and Quantum Information Group at Instituto de Telecomunicações .

Faculty Host: André Platzer

I'll give a brief overview of the PRISM probabilistic model checking system, describe a style of structured model we developed for cyber physical systems, and describe extensions we developed to form< PRISMATIC, a tool that includes statistical model checking, culprit identification, and other tools to help system designers.


Dr. David Musliner is a Senior Principal Research Scientist at Smart Information Flow Technologies (SIFT), LLC. He joined SIFT in 2008. Before that he worked at Honeywell Labs. He completed his 1993PhD in Computer Science/Artificial Intelligence at the University of Michigan, Ann Arbor, and then was a UMIACS postdoctoral fellow, lecturer and Project Director at the University of Maryland Autonomous Mobile Robots Lab.


Many synthesis problems reduce to a common task: Find a structure (e.g. an AST, a finite relation, etc...) with a certain property. It is well-known that constraint solvers are useful for solving this task. The approach is to encode (1) a space of structures with a set of variables and (2) a property as a set of constraints over these variables. However, constraint-based specifications may have (infinitely) many solutions, of which only a few might correspond to distinct solutions to the original synthesis problem. (For example, there are many equivalent programs that differ only by renaming of identifiers.) Consequently, a solver may enumerate many equivalent solutions before visiting a new part of the solution space. Or, it may enumerate distinct solutions in a highly biased manner.

In this talk I present theory and algorithms for better enumeration of solutions using modern constraint solvers. The goal is to first formalize solution enumerators and enumeration bias, and then build algorithms that decrease enumeration bias with modifying the underlying constraint solver. I define an "ideal diverse enumerator" as one that uniformly draws equivalence classes of solutions. Next, I present an algorithm, called "symmetry-directed randomized partitioning", for building empirically diverse enumerators from modern unmodified constraint solvers. Finally, I show that our diverse enumerator is significantly closer to the ideal compared to baseline and randomized solvers.


Ethan K. Jackson is a Researcher in The Research in Software Engineering (RiSE) Group at Microsoft Research. His work focuses on next-generation formal specification languages for model-based development with an emphasis on automated synthesis. He is the developer of the FORMULA language, which has been applied to software, cyber-physical, and biological systems. Ethan received his PhD in Computer Science from Vanderbilt University in 2007 and his BS in Computer Engineering from the University of Pittsburgh in 2004. He joined Microsoft Research in 2007.


Subscribe to CMACS