Parallel Model Checking Algorithms for Linear-Time Temporal Logic

Autor: Barnat, Jiri, Bloemen, Vincent, Duret-Lutz, Alexandre, Laarman, Alfons, Petrucci, Laure, van de Pol, Jaco, Renault, Etienne, Hamadi, Youssef, Sais, Lakhdar

Publikováno v: Handbook of Parallel Constraint Reasoning, 457-507
STARTPAGE=457;ENDPAGE=507;TITLE=Handbook of Parallel Constraint Reasoning
Handbook of Parallel Constraint Reasoning ISBN: 9783319635156
Handbook of Parallel Constraint Reasoning

Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Here, bugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explo

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cef84b08843fd21b258dba5871603470
https://research.utwente.nl/en/publications/68f894f1-2e5c-4b1e-8f4d-04739f68f673