DPO-SYNT: Discrete Control Synthesis for Partially-Observed Systems
New model MPO is available to support the synthesis of centralized sensor activatio policy.
GENERAL USAGE NOTES
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 decribed in [1,2,3,4]. It can handle a large variety of properties, including safety, opacity, diagnosability, detectability, in a uniform manner.
This program contains implementations of BSCOPNBMAX, MPRCP and MPO, as well as a converter utility, defined as follows:
BSCOPNBMAX: Basic Supervisory Control and Observation Problem: Non-blocking and Maximally Permissive Case is the problem of synthesizing non-blocking, deterministic, information-state property compliant, maximally-permissive supervisors for a partially observed Discrete Event System (DES). The problem as well as an algorithmic solution for BSCOPNBMAX are described in  and .
MPO: Most Permissive Observer is a Bipartite Dynamic Observer used to solve Dynamic Sensor Activation Problems for partially observed DES. The structure is utilized in  to synthesize either a maximal or minimal sensor activation policy for an arbitrary information state property.
MPRCP: Maximally-Permissive Supervisors for the Range Control Problem is a problem of synthesizing maximaaly-permissive superviors for a partially-observed Discrete Event System (DES). For now, we consider only safety property. In this mode, we need three FSM inputs, which are G, the original FSM, K, the FSM contains only the safety states and R , the FSM describes the required behavior. The language of R has to be the subset of the language of K. Also, the language of K has to be the subset of the language of G. The three FSMs must satisfy the requirement. This problem is described in .
CONVERT will convert FSM files between the format listed below and the UMDES .fsm file format, which may be useful for viewing structures in DESUMA
- Within this directory in the command terminal, run the command
make. NOTE: this program uses features of C++ unique to C++-11 and later.
- For Windows: you can run DPO-SYNT directly by double clicking
Command line execution of DPO-SYNT is in the form
[-m]- switch between interactive mode
[INTERACTIVE], the BSCOPNBMAX
[no arg], the MPO
[MPO], the MPRCP
[MPRCP]or the converter
[-c]- request the MPO to find a
[-f]- provide an FSM file for processing
[-p]- provide an implemented information state property
[-i]- provide a corresponding file for the specified ISP property
[-r]- provide an required_behavior FSM file for MPRCP mode
[-v]- request more detailed output
[-w]- write all structures relevant to current mode to separate .fsm files in the ./results folder
[-h]- display help menu
Compute supervisor for FSM_test_4.txt w/ safety property and no output
./bin/DES_Supervisor -f ./test/FSM_test_4.txt -p safety -i ./test/safety_test_4.txt
Compute supervisor for FSM_test_6.txt w/ no property and both screen and file output
./bin/DES_Supervisor -f ./test/FSM_test_6.txt -v -w
Compute MPO for FSM_test_2.txt
./bin/DES_Supervisor -f ./test/FSM_test_2.txt -m MPO
Compute maximal MPO for FSM_test_25.fsm w/ state disambiguation property and full output
./bin/DES_Supervisor -f ./test/FSM_test_25.txt -v -w -p disambuguation -i ./test/disambuguation_test_25.txt -m mpo
Compute MPRCP supervisor for test_1.txt w/ the required behavior test_req1.txt, the safety property test_safety1.txt and full output
./bin/DES_Supervisor -m MPRCP -f ./test/test_1.txt -p safety -i ./test/test_safety1.txt -r ./test/test_req1.txt -v
Convert a .txt FSM file to a .fsm FSM file
./bin/DES_Supervisor -f ./test/FSM_test_4.txt -m CONVERT
Start interactive mode
./bin/Des_Supervisor -m interactive
NOTE: All input files should be in Unix format. If unexpected results occur, try running dos2unix on the input files.
FSM_file and Format:
The FSM_file describes the Finite State Machine that will be used to construct the supervisor. Its format is as follows:
<number_of_states> <number_of_events> <state1> <marked (m or u)> ... <staten> <marked (m or u)> <event1> <controllability (c or u)> <observability (o or u)> ... <eventn> <controllability (c or u)> <observability (o or u)> <event state> <event state> ... //state1 transitions ... <event state> <event state> ... //staten transitions
See the FSM_test_.txt and test_ files in the ./test folder for examples. For the Required behavior file, the format is the same as the format of the FSM_file. The events in the Required behavior file have to be the same as the events of the FSM_file.
ISP: The Information State Properties currently defined for this program are safety, opacity, and state disambiguation. See "Adding ISPs" for information on how to add additional ISPs. If this is left blank or does not match any ISP, the supervisor will be constructed with a trivial ISP.
ISP_file: The ISP_file contains additional information specific to the ISP being used in the program. If this is left blank or does not match any file, the supervisor will be constructed with a trivial ISP. For safety, this file contains a list of the unsafe states. For opacity, this file contains a list of secret states. For state disambiguation, this file contains two lines of disjoint states See
./test/<ISP>_test_*.txtfor examples of valid ISP_files. NOTE: The test numbers of the FSM and ISP files in ./test correspond to one another.
Adding ISPs: ISPs are hardcoded in files
./include/IS_Property.has derived classes of class IS_Property. You may use the existing properties as a template to construct your own, or contact the programmer. NOTE: The function get_ISP in the mentioned files must also be modified in order to accept new command line arguments for the new ISP.
Safety for MPRCP: The safety ISP_file for MPRCP is different with other modes. It contains a FSM instead of a list of the unsafe states. The format is the same as the format of the FSM_file. See
./test/test_safety*.txtfor examples of valid safety ISP_files for MPRCP. A set of test files for a single testcase for mode MPRCP is
./test/test_safety*.txt. Also the correspondent output is
Interactive Mode: The default mode of the program is the interactive mode, if there are no arguments. There are instructions shown in this mode. You can type in things according to the instructions.
 Yin, X. and Lafortune, S. (2016). Synthesis of maximally permissive supervisors for partially observed discrete event systems. IEEE Transactions on Automatic Control, 61(5), 1239-1254.
 Yin, X. and Lafortune, S. (2016). A uniform approach for synthesizing property-enforcing supervisors for partially-observed discrete-event systems. IEEE Transactions on Automatic Control, 61(8), 2140-2154.
 Yin, X. and Lafortune, S. (2015). A general approach for solving dynamic sensor activation problems for a class of properties. In Proceedings of the 54th IEEE Conference on Decision and Control, 3610-3615.
 Yin, X. and Lafortune, S. (2016). Synthesis of maximally-permissive supervisors for the range control problem. IEEE Transactions on Automatic Control. DOI: 10.1109/TAC.2016.2644867