Advertisement

Temporal Reasoning on Incomplete Paths

  • Dana FismanEmail author
  • Hillel KuglerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)

Abstract

Semantics of temporal logic over truncated paths (i.e. finite paths that correspond to prefixes of computations of the system at hand) have been found useful in incomplete verification methods (such as bounded model checking and dynamic verification), in modeling hardware resets, and clock shifts and in online and offline monitoring of cyber-physical systems. In this paper we explore providing semantics for temporal logics on other types of incomplete paths, namely incomplete ultimately periodic paths, segmentally broken paths and combinations thereof. We review usages of temporal logic reasoning in systems biology, and explore whether systems biology can benefit from the suggested extensions.

Notes

Acknowledgment

The research was partially supported by the Horizon 2020 research and innovation programme under grant agreement number 732482 (Bio4Comp).

References

  1. 1.
    Ahmed, Z., et al.: Bringing LTL model checking to biologists. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 1–13. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_1CrossRefGoogle Scholar
  2. 2.
    Alon, U.: An Introduction to Systems Biology: Design Principles of Biological Circuits. CRC Press, Boca Raton (2006)zbMATHGoogle Scholar
  3. 3.
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 111–125. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-77395-5_10CrossRefGoogle Scholar
  6. 6.
    Bartocci, E., Bloem, R., Nickovic, D., Roeck, F.: A Counting Semantics for Monitoring LTL Specifications over Finite Traces. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 547–564. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_29CrossRefGoogle Scholar
  7. 7.
    Bartocci, E., Lió, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1), e1004591 (2016)CrossRefGoogle Scholar
  8. 8.
    Batt, G., et al.: Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli. Bioinformatics 21, 19–28 (2005)CrossRefGoogle Scholar
  9. 9.
    Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006).  https://doi.org/10.1007/11944836_25CrossRefzbMATHGoogle Scholar
  10. 10.
    Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Brenner, S.: Sequences and consequences. Philos. Trans. R. Soc. B Biol. Sci. 365(1537), 207–212 (2010)CrossRefGoogle Scholar
  12. 12.
    Cerny, E., Dudani, S., Havlicek, J., Korchemny, D.: SVA: The Power of Assertions in SystemVerilog. Series on Integrated Circuits and Systems. Springer, Heidelberg (2012)Google Scholar
  13. 13.
    Chabrier, N., Fages, F.: Symbolic model checking of biochemical networks. In: Priami, C. (ed.) CMSB 2003. LNCS, vol. 2602, pp. 149–162. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36481-1_13CrossRefGoogle Scholar
  14. 14.
    Chabrier-Rivier, N., Chiaverini, M., Danos, V., Fages, F., Schächter, V.: Modeling and querying biomolecular interaction networks. Theor. Comput. Sci. 325(1), 25–44 (2004)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)CrossRefGoogle Scholar
  16. 16.
    Clavel, M., et al.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71999-1CrossRefzbMATHGoogle Scholar
  17. 17.
    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, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_11CrossRefGoogle Scholar
  18. 18.
    Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45–80 (2001). Preliminary version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS’99)CrossRefGoogle Scholar
  19. 19.
    Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Form. Methods Syst. Des. 51(1), 5–30 (2017)CrossRefGoogle Scholar
  20. 20.
    Dubrova, E., Teslenko, M., Ming, L.: Finding attractors in synchronous multiple-valued networks using SAT-based bounded model checking. In: 40th IEEE International Symposium on Multiple-Valued Logic (ISMVL), pp. 144–149 (2010)Google Scholar
  21. 21.
    Dunn, S.-J., Martello, G., Yordanov, B., Emmott, S., Smith, A.G.: Defining an essential transcription factor program for naïve pluripotency. Science 344(6188), 1156–1160 (2014)CrossRefGoogle Scholar
  22. 22.
    Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45069-6_3CrossRefGoogle Scholar
  23. 23.
    Eisner, C., Fisman, D.: A Practical Introduction to PSL. ICIR. Springer, Boston (2006).  https://doi.org/10.1007/978-0-387-36123-9CrossRefGoogle Scholar
  24. 24.
    Eisner, C., Fisman, D., Havlicek, J.: A topological characterization of weakness. In: Proceedings of the Twenty-Fourth Annual ACM Symposium on Principles of Distributed Computing, PODC 2005, Las Vegas, NV, USA, 17–20 July 2005, pp. 1–8 (2005)Google Scholar
  25. 25.
    Eisner, C., Fisman, D., Havlicek, J.: Safety and liveness, weakness and strength, and the underlying topological relations. ACM Trans. Comput. Log. 15(2), 13:1–13:44 (2014)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Eisner, C., Fisman, D., Havlicek, J., M\(\mathring{a}\)rtensson, J.: The \(\top ,\bot \) approach for truncated semanticsGoogle Scholar
  27. 27.
    Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway logic: symbolic analysis of biological signaling. In Biocomputing 2002, pp. 400–412. World Scientific (2001)Google Scholar
  28. 28.
    Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Talcott, C.: Pathway logic: executable models of biological networks. Electron. Notes Theor. Comput. Sci. 71, 144–161 (2004)CrossRefGoogle Scholar
  29. 29.
    Eker, S., Meseguer, J., Sridharanarayanan, A.: The maude LTL model checker. Electron. Notes Theor. Comput. Sci. 71, 162–187 (2004)CrossRefGoogle Scholar
  30. 30.
    Fauré, A., Naldi, A., Chaouiya, C., Thieffry, D.: Dynamical analysis of a generic Boolean model for the control of the mammalian cell cycle. Bioinformatics 22(14), 124–131 (2006)CrossRefGoogle Scholar
  31. 31.
    Fisman, D.: On the characterization of until as a fixed point under clocked semantics. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 19–33. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-77966-7_6CrossRefGoogle Scholar
  32. 32.
    Furia, C.A., Rossi, M.: No need to be strict: on the expressiveness of metric temporal logics with (non-)strict operators. Bull. EATCS 92, 150–160 (2007)MathSciNetzbMATHGoogle Scholar
  33. 33.
    Furia, C.A., Rossi, M.: On the expressiveness of MTL variants over dense time. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 163–178. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-75454-1_13CrossRefzbMATHGoogle Scholar
  34. 34.
    Gargantini, A., Morzenti, A.: Automated deductive requirements analysis of critical systems. ACM Trans. Softw. Eng. Methodol. 10(3), 255–307 (2001)CrossRefGoogle Scholar
  35. 35.
    Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A.: Statemate; a working environment for the development of complex reactive systems. In: Proceedings of the 10th International Conference on Software Engineering, Singapore, Singapore, 11–15 April 1988, pp. 396–406 (1988)Google Scholar
  36. 36.
  37. 37.
    IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850™Google Scholar
  38. 38.
    IEEE Standard for SystemVerilog – Unified Hardware Design, Specification, and Verification Language, Annex F. IEEE Std 1800™Google Scholar
  39. 39.
    Koymans, R.: Specifying real-time properties with metric temporal logic. R. Time Syst. 2(4), 255–299 (1990)CrossRefGoogle Scholar
  40. 40.
    Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal logic for scenario-based specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31980-1_29CrossRefzbMATHGoogle Scholar
  41. 41.
    Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172–183. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48683-6_17CrossRefGoogle Scholar
  42. 42.
    Le Novère, N.: Quantitative and logic modelling of molecular and gene networks. Nat. Rev. Genet. 16(3), 146–158 (2015)CrossRefGoogle Scholar
  43. 43.
    Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)CrossRefGoogle Scholar
  44. 44.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992).  https://doi.org/10.1007/978-1-4612-0931-7CrossRefzbMATHGoogle Scholar
  45. 45.
    Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., De Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics 24(16), i227–i233 (2008)CrossRefGoogle Scholar
  46. 46.
    Palsson, B.: Systems Biology: Constraint-based Reconstruction and Analysis. Cambridge University Press, Cambridge (2015)CrossRefGoogle Scholar
  47. 47.
    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977, pp. 46–57 (1977)Google Scholar
  48. 48.
    Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985).  https://doi.org/10.1007/BFb0015727CrossRefGoogle Scholar
  49. 49.
  50. 50.
    Tiwari, A., Talcott, C., Knapp, M., Lincoln, P., Laderoute, K.: Analyzing pathways using SAT-based approaches. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) AB 2007. LNCS, vol. 4545, pp. 155–169. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73433-8_12CrossRefGoogle Scholar
  51. 51.
    Traynard, P., Fauré, A., Fages, F., Thieffry, D.: Logical model specification aided by model-checking techniques: application to the mammalian cell cycle regulation. Bioinformatics 32(17), i772–i780 (2016)CrossRefGoogle Scholar
  52. 52.
    Yordanov, B., Dunn, S.-J., Kugler, H., Smith, A., Martello, G., Emmott, S.: A method to identify and analyze biological programs through automated reasoning. NPJ Syst. Biol. Appl. 2, 16010 (2016)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Ben-Gurion UniversityBe’er-ShevaIsrael
  2. 2.Bar-Ilan UniversityRamat-GanIsrael

Personalised recommendations