scholarly journals CheAPS: a Checker of Asynchronous Parameterized Systems

10.29007/d336 ◽  
2018 ◽  
Author(s):  
Igor Konnov
Keyword(s):  
Search Algorithm ◽  
Fixed Number ◽  
Depth First Search ◽  
Parameterized Systems ◽  
Full Version ◽  
The Family ◽  
Fixed Set ◽  
Finite State ◽  
State Models ◽  
Finite State Models

We present CheAPS, the checker of asynchronous parameterized communicating systems. It is a set of tools for verification of parameterized families F = M_n of finite-state models against LTL specification S. Each model M_n from a family F is composed of a fixed number of control processes and n processes from a fixed set of prototypes. Given a description of a family CheAPS generates finite-state models M_n and checks if one of such models can be used as an invariant of the family. As soon as an invariant is detected it is model checked by Spin to verify it against a specification S. If Spin completes the verification successfully, then all the models of F satisfy S.We are going to demonstrate an application of CheAPS to several examples: Chandy-Lamport snapshot algorithm, Awerbuch distributed depth-first search algorithm, Milner's scheduler, and the model of RSVP protocol, where invariants were detected successfully on that models by our tools. The project homepage is http://lvk.cs.msu.su/\~konnov/cheaps/. It is available under BSD-like license.The full version of the abstract is uploaded.

FINITE STATE MODELS WITH BOOLEAN VARIABLES

1968 ◽  
pp. 207-222
Author(s):  
L.E. OSTRANDER ◽  
J.D. SCHOEFFLER ◽  
D.S. GANN
Keyword(s):  
Finite State ◽  
State Models ◽  
Finite State Models

Extended Finite State Models of Language (review)

Language ◽  
2001 ◽  
Vol 77 (3) ◽  
pp. 610-610
Author(s):  
Michael A. Covington
Keyword(s):  
Finite State ◽  
State Models ◽  
Finite State Models

scholarly journals Statistical compression of protein sequences and inference of marginal probability landscapes over competing alignments using finite state models and Dirichlet priors

2019 ◽  
Vol 35 (14) ◽  
pp. i360-i369
Author(s):  
Dinithi Sumanaweera ◽  
Lloyd Allison ◽  
Arun S Konagurthu
Keyword(s):  
Ad Hoc ◽  
Inductive Reasoning ◽  
Protein Sequences ◽  
Information Criterion ◽  
Supplementary Information ◽  
Marginal Probability ◽  
Source Program ◽  
Finite State ◽  
State Models ◽  
Finite State Models

AbstractThe information criterion of minimum message length (MML) provides a powerful statistical framework for inductive reasoning from observed data. We apply MML to the problem of protein sequence comparison using finite state models with Dirichlet distributions. The resulting framework allows us to supersede the ad hoc cost functions commonly used in the field, by systematically addressing the problem of arbitrariness in alignment parameters, and the disconnect between substitution scores and gap costs. Furthermore, our framework enables the generation of marginal probability landscapes over all possible alignment hypotheses, with potential to facilitate the users to simultaneously rationalize and assess competing alignment relationships between protein sequences, beyond simply reporting a single (best) alignment. We demonstrate the performance of our program on benchmarks containing distantly related protein sequences.Availability and implementationThe open-source program supporting this work is available from: http://lcb.infotech.monash.edu.au/seqmmligner.Supplementary informationSupplementary data are available at Bioinformatics online.

Sign in / Sign up

Export Citation Format

Share Document