Resources

Software tools 

If you find some tools missing or you want to add your tool to the list, please forward the link of the tool together with a brief description to xiangyin@umich.edu

Software

Descritpion

Keywords

BZR BZR is a reactive language, belonging to the synchronous languages family, whose main feature is to include discrete controller synthesis within its compilation. It is equipped with a behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part: the semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer. BZR is developed in the Ctrl-A team. FSA, Supervisory Control, Controller Synthesis
DECADA DECADA is a tool for analyzing the control and diagnosis issues in discrete-event systems. FSA,  Fault Diagnosis, Supervisory Control
DECK Discrete Event Control Kit (DECK) is a toolbox (set of M-file functions) written in the programming language of MATLAB for the analysis and design of supervisory control systems based on discrete-event models. Supervisory Control, FSA
DESlab DESlab is a scientific computing program written in python for the development of algorithms for analysis and synthesis of discrete event systems (DES) modeled as automata.

FSA, Supervisory Control

DESpot DESpot is a discrete-event system (DES) software research tool. It supports both flat projects (collection of plant and supervisor DES), and Hierarchical Interface-Based Supervisory Control (HISC) projects. FSA, Supervisory control, Hierarchical
DESUMA The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA).

FSA,  Fault Diagnosis, Supervisory Control

DPO-SYNT DPO-SYNT is a C++ based software toolbox for property enforcement for partially-observed Discrete Event Systems. It implements a recently developed uniform framework for synthesizing maximally-permissive supervisors and optimal sensor activation policies. FSA, Supervisory Control, Sensor Activation
 edisyn EdiSyn is a Python-based toolkit for synthesizing obfuscators that enforces privacy while preserving utility with formal guarantees.

Obfuscator  Synthesis, Privacy Enforcement

ePNK The ePNK is a platform for developing Petri net tools based on the PNML transfer format. Its main idea is to support the definition of Petri net types, which can be easily plugged into it, and to provide a simple generic GMF editor, which can be used for graphically editing nets of any plugged in type. P/T Nets, Model Checking
IDES IDES is a software tool developed at Queen’s University for modeling discrete-event systems and solving discrete-event control systems problems. It allows you to mimic pen-and-paper drawing of state-transition diagrams, export your drawings to a variety of formats such as EPS, JPEG, LaTeX and Grail+, and perform DES operations. FSA, Supervisory Control, Directed Graphs
libFAUDES The discrete event systems library libFAUDES implements data structures and algorithms for finite automata and regular languages. Supervisory control, FSA
MinMaxGD MinMaxGD-a library to handle perioidic series in dioid of formal series. There are a C++ version and an interface with Scicoslab. Max-Plus, Periodic Series in dioid
Roméo Roméo is a software studio for Time Petri Net analysis, developed in the Real-Time Systems Team at IRCCyN . It performs analysis on T-Time Petri nets and on one of their extension to scheduling. Time Petri Nets, Model Checking
PRISM PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. Model Checking, Probabilistic Systems
ReaX ReaX is a tool for controller synthesis of symbolic logico-numerical systems. It makes use of abstract interpretation techniques to handle infinite-state systems (that involve state variables defined on infinite domains such as Integers or Rationals); it also efficiently handles finite-state ones. Controller Synthesis, Infinite-State Systems
SCOTS SCOTS is a tool for the automatic controller synthesis of nonlinear control systems based on symbolic models. The tool accepts a differential equation as the description of a nonlinear control system. It uses a Lipschitz type estimate on the right-hand-side of the differential equation together with a number of discretization parameters to compute a symbolic model. The tool supports the computation of minimal and maximal fixed points and thus natively provides algorithms to synthesize controllers with respect to invariance and reachability specifications. Controller Synthesis, Nonlinear Systems, Symbolic Methods
SENSE SENSE is a tool for the automatic controller synthesis of complex plants in the networked control systems (NCS) based on symbolic models. The tool accepts an existing symbolic model of a nonlinear plant in the NCS and the network characteristics. It computes a symbolic model of the overall networked control system. The tool supports the computation of minimal and maximal fixed points and thus natively provides algorithms to synthesize controllers with respect to invariance and reachability specifications. Controller Synthesis, Networked Systems, Symbolic Methods
Supremica Supremica is a tool for automatic verification and synthesis of controllers for discrete event systems.

Extended-FSA, Synthesis, Abstraction, Verification

SuSyNA This tool allows a user to perform standard supervisor synthesis and time-weighted synthesis plus functions for observer-check and DOT file generation. Supervisor Synthesis, FSA, Time-Weidghted Systems
TAKOS TAKOS stands for Java Toolbox for Analyzing the K-Opacity of Systems dedicated to the analysis, the runtime verification and enforcement of opacity on systems. Opacity, Runtime Verification & Synthesis
TCT TCT is a tool for synthesis of controllers for discrete event systems. FSA, Supervisory Control
TINA TINA (TIme petri Net Analyzer) is a toolbox for the editing and analysis of Petri Nets, with possibly inhibitor and read arcs, Time Petri Nets, with possibly priorities and stopwatches, and an extension of Time Petri Nets with data handling called Time Transition Systems Time Petri Nets, Analysis
TuLiP The Temporal Logic Planning (TuLiP) toolbox is a Python package for automatic synthesis of correct-by-construction embedded control software. Temporal Logic, Synthesis
UPPAAL Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). Timed Automata, Verification
VEiP VEiP is a Java based toolbox for verification and enforcement of opacity properties formulated in Discrete Event Systems. Opacity, Verification, Enforcement
VeriSiMPL This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) models over R^n. Abstractions are characterized as finite-state Labeled Transition Systems (LTS).

MPL Systems, Abstraction 

WOLFGANG Wolfgang is a lightweight tool that allows users to easily create and edit Petri nets and check them against general and workflow specific net properties. P/T-Nets, Colored Petri Nets
  • A more comprehensive list of Petri Nets Tools can be found HERE

  • A more comprehensive list of Model Checkers can be found HERE.

USeful Links 

IFAC Technical Committee 1.3 on Discrete Event and Hybrid Systems

Journal of Discrete Event Dynamic Systems Theory and Applications

Workshop Series on Discrete Event Systems

Petri Nets World