16
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: not found

      Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic

      chapter-article

      Read this article at

      ScienceOpenPublisherPMC
      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          The nonpropositional Metric Temporal Graph Logic (MTGL) specifies the behavior of timed dynamic systems given by timed graph sequences (TGSs), which contain typed attributed graphs representing system states and the elapsed time between states. MTGL satisfaction can be analyzed for finite TGSs by translating its satisfaction problem to the satisfaction problem of nested graph conditions using a folding operation (aggregating a TGS into a graph with history) and a reduction operation (translating an MTGL condition into a nested graph condition).

          In this paper, we introduce an analysis procedure for MTGL to allow for an on-the-fly analysis of finite/infinite TGSs. To this end, we introduce a further (optimistic) reduction of MTGL conditions, which leads to violations during the on-the-fly analysis only when non-satisfaction is guaranteed in the future whereas the former (pessimistic) reduction leads to violations when satisfaction is not guaranteed in the future. We motivate the relevance of our analysis procedure, which uses both reduction operations, by means of a running example. Finally, we discuss prototypical support in the tool AutoGraph.

          Related collections

          Most cited references14

          • Record: found
          • Abstract: not found
          • Article: not found

          Specifying real-time properties with metric temporal logic

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            A brief account of runtime verification

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Modelling and analysis using GROOVE

                Bookmark

                Author and article information

                Contributors
                gadducci@di.unipi.it
                timo.kehrer@informatik.hu-berlin.de
                sven.schneider@hpi.de
                lucas.sakizloglou@hpi.de
                maria.maximova@hpi.de
                holger.giese@hpi.de
                Journal
                978-3-030-51372-6
                10.1007/978-3-030-51372-6
                Graph Transformation
                Graph Transformation
                13th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25–26, 2020, Proceedings
                978-3-030-51371-9
                978-3-030-51372-6
                31 May 2020
                : 12150
                : 276-294
                Affiliations
                [8 ]GRID grid.5395.a, ISNI 0000 0004 1757 3729, Università di Pisa, ; Pisa, Italy
                [9 ]GRID grid.7468.d, ISNI 0000 0001 2248 7639, Humboldt-Universität zu Berlin, ; Berlin, Germany
                GRID grid.500266.7, University of Potsdam, Hasso Plattner Institute, ; Potsdam, Germany
                Author information
                http://orcid.org/0000-0001-9828-618X
                http://orcid.org/0000-0001-6971-1589
                http://orcid.org/0000-0001-9275-806X
                http://orcid.org/0000-0002-4723-730X
                Article
                16
                10.1007/978-3-030-51372-6_16
                7314715
                a1157cb0-5d50-498d-acaa-7bdd83712eef
                © Springer Nature Switzerland AG 2020

                This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.

                History
                Categories
                Article
                Custom metadata
                © Springer Nature Switzerland AG 2020

                graph logic with binding,nonpropositional metric temporal logic,runtime monitoring,three-valued logic

                Comments

                Comment on this article