author = {Wolfgang Schreiner and Ágoston Sütő},
title = {{A Temporal Logic Extension of the RISCAL Model Checker}},
booktitle = {{2022 IEEE 16th International Scientific Conference on Informatics, Poprad, Slovakia, November 23-25}},
language = {english},
abstract = {We report on a new extension of the RISCAL model checker that allows to specify nondeterministic transition systems by formulas in linear temporal logic (LTL) and to verify them under fairness constraints. This extension is based on an automata-theoretic approach to explicit state model checking; the performance of its implementation is in some representative examples competitive with (in fact mostly superior to) that of TLA+, a widely known tool for system modeling and analysis. Thus, while RISCAL was originally developed for describing and analyzing mathematical theories and algorithms over discrete structures, these extensions make RISCAL also a competent checker for formal models of concurrent systems.},
pages = {267--272},
publisher = {IEEE},
isbn_issn = {ISBN 979-8-3503-1034-4},
year = {2022},
editor = {William Steingartner and Štefan Korečko and Anikó Szakál},
refereed = {yes},
keywords = {model checking, first-order logic, linear temporal logic, automata theory, formal specification and verification},
sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},
length = {6},
url = {https://doi.org/10.1109/Informatics57926.2022.10083433}