Name
Abstract | ||
|---|---|---|
G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into executable code for a large number of industrial field-level devices. The synthesis algorithm of G4LTL-ST implements pseudo-Boolean abstraction of data constraints and the compilation of timing constraints into LTL, together with a counterstrategy-guided abstraction-refinement synthesis loop. Since temporal logic specifications are notoriously difficult to use in practice, G4LTL-ST supports engineers in specifying realizable control problems by suggesting suitable restrictions on the behavior of the control environment from failed synthesis attempts. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-08867-9_36 | CAV |
Keywords | DocType | Volume |
industrial automation, synthesis, theory combination, assumption generation | Journal | abs/1405.2409 |
ISSN | Citations | PageRank |
0302-9743 | 8 | 0.57 |
References | Authors | |
17 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chih-Hong Cheng | 1 | 134 | 17.63 |
| Chung-Hao Huang | 2 | 85 | 7.55 |
| Harald Ruess | 3 | 95 | 10.86 |
| Stefan Stattelmann | 4 | 95 | 6.98 |