Wolfgang Schreiner, Ágoston Sütö,
"A Temporal Logic Extension of the RISCAL Model Checker"
, in William Steingartner, ?tefan Kore?ko, Anikó Szakál: 2022 IEEE 16th International Scientific Conference on Informatics, Poprad, Slovakia, November 23-25, IEEE, Seite(n) 267--272, 2022, ISBN: 979-8-3503-1034-4
A Temporal Logic Extension of the RISCAL Model Checker
Sprache des Titels:
2022 IEEE 16th International Scientific Conference on Informatics, Poprad, Slovakia, November 23-25
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.