State Identification and Verification with Satisfaction

Joshua Moerman; Thorsten Wißmann

doi:10.1007/978-3-031-15629-8_23

State Identification and Verification with Satisfaction

Joshua Moerman^*, Thorsten Wißmann

^*Corresponding author for this work

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

Abstract

We use SAT-solving to construct adaptive distinguishing sequences and unique input/output sequences for finite state machines in the flavour of Mealy machines. These sequences solve the state identification and state verification problems respectively. Preliminary experiments evaluate our implementation and show that this approach via SAT-solving works well and is able to find many short sequences.

Original language	English
Title of host publication	A Journey from Process Algebra via Timed Automata to Model Learning
Subtitle of host publication	Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday
Editors	Nils Jansen, Mariëlle Stoelinga, Petra van den Bos
Publisher	Springer
Pages	450-466
Number of pages	17
Volume	13560
Edition	1
ISBN (Electronic)	978-3-031-15629-8
ISBN (Print)	978-3-031-15628-1
DOIs	https://doi.org/10.1007/978-3-031-15629-8_23
Publication status	Published - 7 Sept 2022

Publication series

Series	Lecture Notes in Computer Science
Volume	13560
ISSN	0302-9743

Keywords

Conformance Testing
Finite State Machines
Mealy machines
SAT solving
State Identification

Access to Document

10.1007/978-3-031-15629-8_23

1 Software

satuio: Software tool for generating adaptive distinguishing sequences and unique input/output sequences for finite state machines
Moerman, J. & Wißmann, T., 23 Sept 2022
Research output: Non-textual form › Software › Academic

Open Access

Cite this

Moerman, J., & Wißmann, T. (2022). State Identification and Verification with Satisfaction. In Nils Jansen, Mariëlle Stoelinga, & Petra van den Bos (Eds.), A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday (1 ed., Vol. 13560, pp. 450-466). Springer. https://doi.org/10.1007/978-3-031-15629-8_23

Moerman, Joshua ; Wißmann, Thorsten. / State Identification and Verification with Satisfaction. A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. editor / Nils Jansen ; Mariëlle Stoelinga ; Petra van den Bos. Vol. 13560 1. ed. Springer, 2022. pp. 450-466 (Lecture Notes in Computer Science, Vol. 13560).

@inbook{91482143a20c437987a2f78cdf1f0267,

title = "State Identification and Verification with Satisfaction",

abstract = "We use SAT-solving to construct adaptive distinguishing sequences and unique input/output sequences for finite state machines in the flavour of Mealy machines. These sequences solve the state identification and state verification problems respectively. Preliminary experiments evaluate our implementation and show that this approach via SAT-solving works well and is able to find many short sequences.",

keywords = "Conformance Testing, Finite State Machines, Mealy machines, SAT solving, State Identification",

author = "Joshua Moerman and Thorsten Wi{\ss}mann",

note = "DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2022",

month = sep,

day = "7",

doi = "10.1007/978-3-031-15629-8_23",

language = "English",

isbn = "978-3-031-15628-1",

volume = "13560",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "450--466",

editor = "{Nils Jansen} and {Mari{\"e}lle Stoelinga} and {Petra van den Bos}",

booktitle = "A Journey from Process Algebra via Timed Automata to Model Learning",

edition = "1",

}

Moerman, J & Wißmann, T 2022, State Identification and Verification with Satisfaction. in Nils Jansen, Mariëlle Stoelinga & Petra van den Bos (eds), A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. 1 edn, vol. 13560, Springer, Lecture Notes in Computer Science, vol. 13560, pp. 450-466. https://doi.org/10.1007/978-3-031-15629-8_23

State Identification and Verification with Satisfaction. / Moerman, Joshua; Wißmann, Thorsten.
A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. ed. / Nils Jansen; Mariëlle Stoelinga; Petra van den Bos. Vol. 13560 1. ed. Springer, 2022. p. 450-466 (Lecture Notes in Computer Science, Vol. 13560).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - State Identification and Verification with Satisfaction

AU - Moerman, Joshua

AU - Wißmann, Thorsten

N1 - DBLP License: DBLP's bibliographic metadata records provided through http://dblp.org/ are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2022/9/7

Y1 - 2022/9/7

N2 - We use SAT-solving to construct adaptive distinguishing sequences and unique input/output sequences for finite state machines in the flavour of Mealy machines. These sequences solve the state identification and state verification problems respectively. Preliminary experiments evaluate our implementation and show that this approach via SAT-solving works well and is able to find many short sequences.

AB - We use SAT-solving to construct adaptive distinguishing sequences and unique input/output sequences for finite state machines in the flavour of Mealy machines. These sequences solve the state identification and state verification problems respectively. Preliminary experiments evaluate our implementation and show that this approach via SAT-solving works well and is able to find many short sequences.

KW - Conformance Testing

KW - Finite State Machines

KW - Mealy machines

KW - SAT solving

KW - State Identification

U2 - 10.1007/978-3-031-15629-8_23

DO - 10.1007/978-3-031-15629-8_23

M3 - Chapter

SN - 978-3-031-15628-1

VL - 13560

T3 - Lecture Notes in Computer Science

SP - 450

EP - 466

BT - A Journey from Process Algebra via Timed Automata to Model Learning

A2 - Nils Jansen,

A2 - Mariëlle Stoelinga,

A2 - Petra van den Bos,

PB - Springer

ER -

Moerman J, Wißmann T. State Identification and Verification with Satisfaction. In Nils Jansen, Mariëlle Stoelinga, Petra van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning: Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday. 1 ed. Vol. 13560. Springer. 2022. p. 450-466. (Lecture Notes in Computer Science, Vol. 13560). doi: 10.1007/978-3-031-15629-8_23

State Identification and Verification with Satisfaction

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Research output

satuio: Software tool for generating adaptive distinguishing sequences and unique input/output sequences for finite state machines

Cite this