caa a22 4500 475797523 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000301xx s 000 0 eng 10.1023/A:1008743212620 doi (NATIONALLICENCE)springer-10.1023/A:1008743212620 Verification of Safety Properties Using Integer Programming: Beyond the State Equation [Elektronische Daten] [Javier Esparza, Stephan Melzer] The state equation is a verification technique that has been applied—not always under this name—to numerous systems modelled as Petri nets or communicating automata. Given a safety property P, the state equation is used to derive a necessary condition for P to hold which can be mechanically checked. The necessary conditions derived from the state equation are known to be of little use for systems communicating by means of shared variables, in the sense that many of these systems satisfy the property but not the conditions. In this paper, we use traps, a well-known notion of net theory, to obtain stronger conditions that can still be efficiently checked. We show that the new conditions significantly extend the range of verifiable systems. Kluwer Academic Publishers, 2000 state equation nationallicence traps nationallicence approximation techniques nationallicence linear programming nationallicence Esparza Javier Institut für Informatik, Technische Universität München, Arcisstr. 21, 80290, München, Germany aut Melzer Stephan Institut für Informatik, Technische Universität München, Arcisstr. 21, 80290, München, Germany aut Formal Methods in System Design Kluwer Academic Publishers 16/2(2000-03-01), 159-189 0925-9856 16:2<159 2000 16 10703 https://doi.org/10.1023/A:1008743212620 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008743212620 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Esparza Javier Institut für Informatik, Technische Universität München, Arcisstr. 21, 80290, München, Germany aut NATIONALLICENCE 700 1- Melzer Stephan Institut für Informatik, Technische Universität München, Arcisstr. 21, 80290, München, Germany aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/2(2000-03-01), 159-189 0925-9856 16:2<159 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer