Repository logo
 

Bringing LTL Model Checking to Biologists

Accepted version
Peer-reviewed

Type

Book chapter

Change log

Authors

Ahmed, Z 
Benque, D 
Berezin, S 
Dahl, ACE 
Fisher, Jasmin 

Abstract

The BioModelAnalyzer (BMA) is a web based tool for the development of discrete models of biological systems. Through a graphical user interface, it allows rapid development of complex models of gene and protein interaction networks and stability analysis without requiring users to be proficient computer programmers. Whilst stability is a useful specification for testing many systems, testing temporal specifications in BMA presently requires the user to perform simulations. Here we describe the LTL module, which includes a graphical and natural language interfaces to testing LTL queries. The graphical interface allows for graphical construction of the queries and presents results visually in keeping with the current style of BMA. The Natural language interface complements the graphical interface by allowing a gentler introduction to formal logic and exposing educational resources.

Description

Title

Bringing LTL Model Checking to Biologists

Keywords

Is Part Of

Book type

Publisher

Springer

ISBN

Sponsorship
Royal Society (Paul Instrument Fund) (UF130039)
MRC (unknown)
MRC (MC_UU_12022/9)
MRC ()