Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking

Metadata Updated: November 12, 2020

The translation of temporal logic specifications constitutes an essen- tial step in model checking and a major influence on the efficiency of formal verification via model checking. We devise a new explicit-state translation of Lin- ear Temporal Logic to automata for the class of LTL specifications that describe safety properties, arguably the most used formal specifications in real-world sys- tems. By exploiting the inherent determinism in safety specifications, we can build deterministic Promela never claims that accept only the bad prefixes of the safety specification. In contrast to previous works, we focus on compilation to never claims rather than simply automata and measure Spin model-checking time separately from compilation time and automata size. An extensive experi- mental evaluation over a space of configurations demonstrates that our new trans- lation consistently results in better model-checking performance, for a large array of benchmarks, over the best current translation.

Access & Use Information

Public: This dataset is intended for public access and use. License: No license information was provided. If this work was prepared by an officer or employee of the United States government as part of that person's official duties it is considered a U.S. Government Work.

Downloads & Resources


Metadata Created Date November 12, 2020
Metadata Updated Date November 12, 2020
Data Update Frequency irregular

Metadata Source

Harvested from NASA Data.json

Additional Metadata

Resource Type Dataset
Metadata Created Date November 12, 2020
Metadata Updated Date November 12, 2020
Publisher Dashlink
Unique Identifier Unknown
Identifier DASHLINK_706
Data First Published 2013-04-25
Data Last Modified 2020-01-29
Public Access Level public
Data Update Frequency irregular
Bureau Code 026:00
Metadata Context
Metadata Catalog ID
Schema Version
Catalog Describedby
Homepage URL
Program Code 026:029
Source Datajson Identifier True
Source Hash 9ccb5343893e584a57d885e7e4bb849e2a4f5b93
Source Schema Version 1.1

Didn't find what you're looking for? Suggest a dataset here.