Generating and Employing Witness Automata for ACTLW Formulae
When verifying the validity of a formula in a system model by a model checker, a common feature is the generation of a linear witness or counterexample, which is a computation path usually showing a single reason why the formula is valid or, respectively, not. For systems represented with Labeled Tr...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2022-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/9681848/ |
| _version_ | 1798024898884403200 |
|---|---|
| author | Rok Vogrin Robert Meolic Tatjana Kapus |
| author_facet | Rok Vogrin Robert Meolic Tatjana Kapus |
| author_sort | Rok Vogrin |
| collection | DOAJ |
| description | When verifying the validity of a formula in a system model by a model checker, a common feature is the generation of a linear witness or counterexample, which is a computation path usually showing a single reason why the formula is valid or, respectively, not. For systems represented with Labeled Transition Systems (LTS) and a subset of ACTLW (Action-based Computation Tree Logic with Unless operator) formulae, a procedure exists for the generation of witness automata, which contain all the interesting finite linear witnesses, thus revealing all the reasons of the validity of a formula. Although this procedure uses a symbolic representation of LTSs, transitions of a given LTS are traversed one by one. In this paper, we propose a procedure which exploits the symbolic representation efficiently to traverse several transitions at once. We evaluate the procedure on models of a communication protocol from industry and a biological system. The results show it to be at least several times faster than the former one. Witness automata were first introduced to allow for compositional generation of test sequences. We propose two more possible uses. One is for the detection of multiple errors in a model by exploring the witness automaton for a formula, instead of only one, which is usually the case with a single witness. The other one is for the detection of previously unknown system properties. As witness automata can be rather large, we show how some existing tools could help in examining them through visualization and simulation. |
| first_indexed | 2024-04-11T18:10:02Z |
| format | Article |
| id | doaj.art-b6effe5596994c718af61f7a5d062107 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-04-11T18:10:02Z |
| publishDate | 2022-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-b6effe5596994c718af61f7a5d0621072022-12-22T04:10:11ZengIEEEIEEE Access2169-35362022-01-01109889990510.1109/ACCESS.2022.31434789681848Generating and Employing Witness Automata for ACTLW FormulaeRok Vogrin0https://orcid.org/0000-0001-5701-4671Robert Meolic1https://orcid.org/0000-0003-3395-1227Tatjana Kapus2https://orcid.org/0000-0003-3228-3941Faculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, SloveniaOperato, Maribor, SloveniaFaculty of Electrical Engineering and Computer Science, University of Maribor, Maribor, SloveniaWhen verifying the validity of a formula in a system model by a model checker, a common feature is the generation of a linear witness or counterexample, which is a computation path usually showing a single reason why the formula is valid or, respectively, not. For systems represented with Labeled Transition Systems (LTS) and a subset of ACTLW (Action-based Computation Tree Logic with Unless operator) formulae, a procedure exists for the generation of witness automata, which contain all the interesting finite linear witnesses, thus revealing all the reasons of the validity of a formula. Although this procedure uses a symbolic representation of LTSs, transitions of a given LTS are traversed one by one. In this paper, we propose a procedure which exploits the symbolic representation efficiently to traverse several transitions at once. We evaluate the procedure on models of a communication protocol from industry and a biological system. The results show it to be at least several times faster than the former one. Witness automata were first introduced to allow for compositional generation of test sequences. We propose two more possible uses. One is for the detection of multiple errors in a model by exploring the witness automaton for a formula, instead of only one, which is usually the case with a single witness. The other one is for the detection of previously unknown system properties. As witness automata can be rather large, we show how some existing tools could help in examining them through visualization and simulation.https://ieeexplore.ieee.org/document/9681848/Automataformal verificationlogicmodel checking |
| spellingShingle | Rok Vogrin Robert Meolic Tatjana Kapus Generating and Employing Witness Automata for ACTLW Formulae IEEE Access Automata formal verification logic model checking |
| title | Generating and Employing Witness Automata for ACTLW Formulae |
| title_full | Generating and Employing Witness Automata for ACTLW Formulae |
| title_fullStr | Generating and Employing Witness Automata for ACTLW Formulae |
| title_full_unstemmed | Generating and Employing Witness Automata for ACTLW Formulae |
| title_short | Generating and Employing Witness Automata for ACTLW Formulae |
| title_sort | generating and employing witness automata for actlw formulae |
| topic | Automata formal verification logic model checking |
| url | https://ieeexplore.ieee.org/document/9681848/ |
| work_keys_str_mv | AT rokvogrin generatingandemployingwitnessautomataforactlwformulae AT robertmeolic generatingandemployingwitnessautomataforactlwformulae AT tatjanakapus generatingandemployingwitnessautomataforactlwformulae |