ACTS--A Concurrency Tool Suite

The ACTS project involves the development of software that applies methods of supervisory control to the automatic synthesis of concurrent programs. Supervisory control is applied here in order to address issues arising in the context of concurrency, such as mutual exclusion, liveness, and fairness. Specifications are processed in three stages, as follows. First, based on an input describing concurrent processes, synchronization constraints, and other requirements, the software obtains a Petri net model. Second, supervisory control methods are applied in order to the control specifications. Finally, based on the specified description of the concurrent processes and the control logic synthesized by the supervisory control methods, code is generated. While this approach is not limited to a particular language or operating system, at this time the software is written for Unix and the C language.

The project has involved LeTourneau University and University of Notre Dame. The support of the National Science Fundation is gratefully acknowledged (NSF CNS-0834057).

The file contains the source code of version 1.2 (August 2012), which is the most recent version of the software. To get started using the software, please refer to the information presented in the documentation directory and the example directory of the source code. Earlier versions of the software may be found at

References related to this work are as follows.

While this project is not limited to a particular set of methods of supervisory control, currently the software implements the supervision based on place invariants. Various other methods are likely to be considered in future work. The following are the main references of the supervisory control methods that are currently implemented in the software.

The supervisory control functions of the software are a C-language version of the SPNBOX toolbox.

Last modified: Tue May 14 10:49:39 CDT 2013