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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
To the best of our knowledge, most LTL tools do not support such a direct comparison between the value of a variable and its value in the next state.
References
Bonzanni, N., Garg, A., Feenstra, K.A., Schütte, J., Kinston, S., Miranda-Saavedra, D., Heringa, J., Xenarios, I., Göttgens, B.: Hard-wired heterogeneity in blood stem cells revealed using a dynamic regulatory network model. Bioinformatics 29, i80–i88 (2013)
Chuang, R., Hall, B., Benque, D., Cook, B., Ishtiaq, S., Piterman, N., Taylor, A., Vardi, M., Koschmieder, S., Gottgens, B., Fisher, J.: Drug target optimization in chronic myeloid leukemia using innovative computational platform. Sci. Rep. 5, 8190 (2015)
Moignard, V., Woodhouse, S., Haghverdi, L., Lilly, J., Tanaka, Y., Wilkinson, A., Buettner, F., Nishikawa, S., Piterman, N., Kouskoff, V., Theis, F., Fisher, J., Gottgens, B.: Decoding the regulatory network of early blood development from single cell gene expression measurements. Nat. Biotechnol. 33, 269–276 (2015)
Remy, E., Rebouissou, S., Chaouiya, C., Zinovyev, A., Radvanyi, F., Calzone, L.: A modeling approach to explain mutually exclusive and co-occurring genetic alterations in bladder tumorigenesis. Cancer Res. 75, 4042–4052 (2015)
Terfve, C.D.A., Wilkes, E.H., Casado, P., Cutillas, P.R., Saez-Rodriguez, J.: Large-scale models of signal propagation in human cells derived from discovery phosphoproteomic data. Nat. Commun. 6, 8033 (2015)
Benque, D., et al.: BMA: visual tool for modeling and analyzing biological networks. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 686–692. Springer, Berlin (2012). doi:10.1007/978-3-642-31424-7_50
Naldi, A., Thieffry, D., Chaouiya, C.: Decision diagrams for the representation and analysis of logical models of genetic networks. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS, vol. 4695, pp. 233–247. Springer, Berlin (2007). doi:10.1007/978-3-540-75140-3_16
Cook, B., Fisher, J., Krepska, E., Piterman, N.: Proving stabilization of biological systems. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 134–149. Springer, Berlin (2011). doi:10.1007/978-3-642-18275-4_11
Cook, B., Fisher, J., Hall, B.A., Ishtiaq, S., Juniwal, G., Piterman, N.: Finding instability in biological models. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 358–372. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_24
Claessen, K., Fisher, J., Ishtiaq, S., Piterman, N., Wang, Q.: Model-checking signal transduction networks through decreasing reachability sets. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 85–100. Springer, Berlin (2013). doi:10.1007/978-3-642-39799-8_5
Schaub, M., Henzinger, T., Fisher, J.: Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC Syst. Biol. 1, 4 (2007)
Bean, D., Heimbach, J., Ficorella, L., Micklem, G., Oliver, S., Favrin, G.: esyN: Network building, sharing, and publishing. PLoS ONE 9, e106035 (2014)
Microsoft: Microsoft bot framework (2016). https://dev.botframework.com/
Microsoft: Microsoft cognitive services (2016). https://www.microsoft.com/cognitive-services/
SAP: Chevrotain a JavaScript parsing DSL (2014). https://github.com/SAP/chevrotain/
van der Plas, L., Tiedemann, J.: Finding synonyms using automatic word alignment and measures of distributional similarity. In: Proceedings of the COLING/ACL on Main Conference Poster Sessions. COLING-ACL 2006, Stroudsburg, PA, USA, pp. 866–873. Association for Computational Linguistics (2006)
Richardson, R., Smeaton, A., Murphy, J.: Using wordnet as a knowledge base for measuring semantic similarity between words (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Ahmed, Z. et al. (2017). Bringing LTL Model Checking to Biologists. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-52234-0_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-52233-3
Online ISBN: 978-3-319-52234-0
eBook Packages: Computer ScienceComputer Science (R0)