Model checking games and a genome sequence search

Autor:	S M Staroletov
Rok vydání:	2020
Předmět:	Model checking History Theoretical computer science Computer science Hash function String searching algorithm Construct (python library) ENCODE Fuzzy logic Computer Science Applications Education Promela Transition system computer computer.programming_language
Zdroj:	Journal of Physics: Conference Series. 1679:032020
ISSN:	1742-6596 1742-6588
DOI:	10.1088/1742-6596/1679/3/032020
Popis:	The paper is considered a concept of model checking games to solve algorithmic puzzles. We describe current approaches in this field and move to a game between a user and a software model checker with the goal to provide a solution to a problem, encoded in a transition system and an LTL formula with a requirement. We show how to encode and solve some problems using this approach. Then we move to the problem of searching a pattern in a genome sequence. We implement the Z-function search method in Promela, construct the model, provide the input of real viral data, and then play a model checking game with SPIN verifier. We created a fuzzy substring search method using the non-deterministic choice operator. Based on experiments we made, we discuss that the problem to find a pattern with some deviations is only solvable using the swarm verification and hash compact methods.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::7984bcbc9ec7e80ce7d484419ad38991 https://doi.org/10.1088/1742-6596/1679/3/032020 Zobrazit plný text záznamu