State Identification and Verification with Satisfaction
7 Sep 2022
Joshua Moerman and Thorsten Wißmann
Frits'60
This paper is dedicated to Frits Vaandrager on the occasion of his 60th birthday and bundled in A Journey from Process Algebra via Timed Automata to Model Learning.
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.