Tools:
- K-Step Opacity Benchmarks
- Initial-and-final-state opacity benchmarks
- Coordination Control Plug-In
for libFAUDES C++ library
(distributed under conditions of the GNU Lesser General Public License
LGPL)
Version: released on Feb 5, 2012. Included in the official libFAUDES distribution since version 2.21e.
Description: Complete coordination control synthesis procedure for the computation of
the supremal conditionally controllable sublanguage of a given prefix-closed global specification language K
and a set of local subsystems, corresponding supervisors, and the supervised coordinator.
(The case of non-prefix-closed global specifications is under investigation...)
Updates:
- Polynomial algorithm for conditional decomposability included since version 2.26
- Piecewise testability Plug-In
for libFAUDES C++ library
(distributed under conditions of the GNU Lesser General Public License
LGPL)
Author: Eliška Foltasová
Description: This tool implements three algorithms to verify piecewise testability.
The tool is a plug-in for the C++ library libFAUDES.
- Relative observability Plug-In
for libFAUDES C++ library
(distributed under conditions of the GNU Lesser General Public License
LGPL)
Author: Marián Pochyba
Description:
This tool implements the algorithms for verification of observability and relative observability of systems (languages)
represented by finite automata as a plug-in for the C++ library libFAUDES.
- Co-developer of the web portal for the International Center for Computational Logic
at TU Dresden, 2014. Powered by MediaWiki and Semantic MediaWiki.