NYCS: Naples hYbrid Controller Synthesis

NYCS is a tool for solving the controllability problem for Linear Hybrid Games (LHGs) with safety and reachability goals.

Basic usage

NYCS is run from the command line with two arguments: a model file and a configuration file. 
	  nycs <model file> <configuration file>
Example: 
	  nycs maze_5_deterministic_flow.xml maze.cfg.xml
Syntax of the model files
Syntax of the configuration files

Graphical Front-end: polyview

Polyview is a Java application displaying 2D sections and projections of polyhedra having an arbitrary number of dimensions.

Graphical Front-end: poly2tex

poly2tex is a command-line tool converting polyhedra into 2D LaTeX pgf figures. Similarly to polyview, you should set the value of all variables, except two, which are plotted into a 2D drawing. Instead of setting a constant value, a variable can be existentially quantified (i.e., projected away).

Downloads

Virtual machine for Oracle Virtualbox: Download (1.8 GB)

Quick start:

  1. Log in as "nycs", password "synthesis" (if requested).
  2. Open terminal (e.g., LXTerminal on desktop)
  3. 	      > nycs nycs/examples/reachability/maze/maze_5_deterministic_flow.xml nycs/examples/reachability/maze/maze.cfg.xml | split.sh
	      > polyview
  4. In polyview, choose File -> Open in new tab -> "N.poly"
  5. In polyview, tick the "x" and "y" boxes under the "View 1" column

Sources

The NYCS parser contains code from the SpaceEx project, which we gratefully acknowledge.

Credits

Main developers: Marco Faella and Massimo Benerecetti

Contributors: Stefano Minopoli, Valeria Tedesco, Pietro Neroni, Donatella Eramo, Aniello Sorrentino (polyview), Marco Urbano.

Bibliography

  • M. Benerecetti, M. Faella
    "Tracking Smooth Trajectories in Linear Hybrid Systems"
    Information and Computation, vol. 257, p. 114-138, Elsevier 2017.
    Download:    PDF
  • M. Benerecetti, M. Faella
    "Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Reachability Control"
    ACM Transactions on Embedded Computing Systems, vol. 16 (4), 2017.
    Download:    PDF
  • M. Benerecetti, M. Faella, S. Minopoli
    "Automatic Synthesis of Switching Controllers for Linear Hybrid Systems: Safety Control",
    Theoretical Computer Science, 493, p. 116-138. Elsevier, 2013.
    DOI: 10.1016/j.tcs.2012.10.042
    Download:    PDF
  • M. Benerecetti, M. Faella
    "Tracking Differentiable Trajectories across Polyhedra Boundaries",
    HSCC 2013, 16th International Conference on Hybrid Systems: Computation and Control.
    Philadelphia, USA, April 2013.
    Download:    PDF   
  • M. Benerecetti, M. Faella, S. Minopoli
    "Reachability Games for Linear Hybrid Systems",
    HSCC 2012, 15th International Conference on Hybrid Systems: Computation and Control.
    Beijing, China, April 2012.
    DOI: 10.1145/2185632.2185645
    Download:    PDF   
  • M. Benerecetti, M. Faella, S. Minopoli
    "Revisiting Synthesis of Switching Controllers for Linear Hybrid Systems",
    CDC 2011, 50th IEEE Conference on Decision and Control.
    Orlando, FL, USA, December 2011.
    Download:    PDF   
    Extended by the journal paper "Automatic synthesis of switching controllers for linear hybrid systems: safety control"
  • M. Benerecetti, M. Faella, S. Minopoli
    "Towards Efficient Exact Synthesis for Linear Hybrid Systems",
    GandALF 2011, Second International Symposium on Games, Automata, Logics and Formal Verification.
    Minori, Salerno, Italy, June 2011.
    EPTCS 54.
    DOI: 10.4204/EPTCS.54.19.
    Download:    PDF   
    Extended by the journal paper "Automatic synthesis of switching controllers for linear hybrid systems: safety control"