Cyber-physical systems often encompass complex concurrent behavior with timing constraints and probabilistic failures on demand. The analysis whether such systems with probabilistic timed behavior adhere to a given specification is essential. When the states of the system can be represented by graphs, the rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) can be used to suitably capture structure dynamics as well as probabilistic and timed behavior of the system. The model checking support for PTGTSs w.r.t. properties specified using Probabilistic Timed Computation Tree Logic (PTCTL) has been already presented. Moreover, for timed graph-based runtime monitoring, Metric Temporal Graph Logic (MTGL) has been developed for stating metric temporal properties on identified subgraphs and their structural changes over time. In this paper, we (a) extend MTGL to the Probabilistic Metric Temporal Graph Logic (PMTGL) by allowing for the specification of probabilistic properties, (b) adapt our MTGL satisfaction checking approach to PTGTSs, and (c) combine the approaches for PTCTL model checking and MTGL satisfaction checking to obtain a Bounded Model Checking (BMC) approach for PMTGL. In our evaluation, we apply an implementation of our BMC approach in AutoGraph to a running example.
Various kinds of typed attributed graphs are used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformations provide a formal model for defining state sequences. We consider the extended case where time elapses between states and introduce a logic to reason about these sequences. With this logic we express properties on the structure and attributes of states as well as on the temporal occurrence of states that are related by their inner structure, which no formal logic over graphs accomplishes concisely so far. Firstly, we introduce graphs with history by equipping every graph element with the timestamp of its creation and, if applicable, its deletion. Secondly, we define a logic on graphs by integrating the temporal operator until into the well-established logic of nested graph conditions. Thirdly, we prove that our logic is equally expressive to nested graph conditions by providing a suitable reduction. Finally, the implementation of this reduction allows for the tool-based analysis of metric temporal properties for state sequences. Verschiedene Arten von getypten attributierten Graphen werden benutzt, um Zustände von Systemen in vielen unterschiedlichen Anwendungsbereichen zu beschreiben. Der etablierte Formalismus der Graphtransformationen bietet ein formales Model, um Zustandssequenzen für dynamische Systeme zu definieren. Wir betrachten den erweiterten Fall von solchen Sequenzen, in dem Zeit zwischen zwei verschiedenen Systemzuständen vergeht, und führen eine Logik ein, um solche Sequenzen zu beschreiben. Mit dieser Logik drücken wir zum einen Eigenschaften über die Struktur und die Attribute von Zuständen aus und beschreiben zum anderen temporale Vorkommen von Zuständen, die durch ihre innere Struktur verbunden sind. Solche Eigenschaften können bisher von keiner der existierenden Logiken auf Graphen vergleichbar darstellt werden. Erstens führen wir Graphen mit Änderungshistorie ein, indem wir jedes Graphelement mit einem Zeitstempel seiner Erzeugung und, wenn nötig, seiner Löschung versehen. Zweitens definieren wir eine Logik auf Graphen, indem wir den Temporaloperator Until in die wohl-etablierte Logik der verschachtelten Graphbedingungen integrieren. Drittens beweisen wir, dass unsere Logik gleich ausdrucksmächtig ist, wie die Logik der verschachtelten Graphbedingungen, indem wir eine passende Reduktionsoperation definieren. Zuletzt erlaubt uns die Implementierung dieser Reduktionsoperation die werkzeukbasierte Analyse von metrisch-temporallogischen Eigenschaften für Zustandssequenzen zu führen.
Technical Report from the year 2016 in the subject Art - Overall Considerations, grade: A COST Case Study, , course: Cost Action TD1201 Working Group Meetings; 5th international Culture Forum St. Peterburg December 2016, language: English, abstract: This complex investigation by European and Russian experts was carried out for the purpose of solving the question of the authorship and date of the Archangel icon kept in the National Museum in Belgrade and attributed to the 15th c Novgorod school. It had also the task to explore the possibilities and limits of non-destructive methods in identification, dating and authentication of icon painting, as well as of other types of historic easel painting. In addition to the various technological methods, the research project included assessment of the outcomes on base of additional information from databases accumulated by leading research and restoration centers in Russia and Eastern Europe. The authors' purpose was to demonstrate that actually the conditions for authenticity controls are easily available, and that they can be realized at an enough competitively level, making better use of already accumulated experience and using a more common technological base. Particularly important is to underline that tools for efficient non-contact investigation of artefacts are not exclusively the optical techniques and the utilized instruments for themselves, but also the way in which the various data they produce have been assessed. For to transform these informational resources in real knowledge, their mass storage and interactive art historical, technical and technological assessment is of fundamental importance. The non-destructive methods and techniques used included optical microscopy, macro photography in VIS/raking light, stereo microscopy, ultraviolet luminescence/fluorescence, infrared reflectography, X-ray, EDXRFS, computer tomography, anatomical analysis of wood, micro chemical analysis, and were followed by a comparison and post processing of obtained data and images, allowing to date the icon at the second half of the 19th century (the earlier attribution was 15th century). The icon may have been created by icon painters of the southern regions of the Russian Empire (perhaps in Moldova or Ukraine). The results created the conditions for a detailed mapping of its status of conservation and were indispensable for to understand the origin of the damages.
Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update.
Various kinds of typed attributed graphs are used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformations provide a formal model for defining state sequences. We consider the extended case where time elapses between states and introduce a logic to reason about these sequences. With this logic we express properties on the structure and attributes of states as well as on the temporal occurrence of states that are related by their inner structure, which no formal logic over graphs accomplishes concisely so far. Firstly, we introduce graphs with history by equipping every graph element with the timestamp of its creation and, if applicable, its deletion. Secondly, we define a logic on graphs by integrating the temporal operator until into the well-established logic of nested graph conditions. Thirdly, we prove that our logic is equally expressive to nested graph conditions by providing a suitable reduction. Finally, the implementation of this reduction allows for the tool-based analysis of metric temporal properties for state sequences. Verschiedene Arten von getypten attributierten Graphen werden benutzt, um Zustände von Systemen in vielen unterschiedlichen Anwendungsbereichen zu beschreiben. Der etablierte Formalismus der Graphtransformationen bietet ein formales Model, um Zustandssequenzen für dynamische Systeme zu definieren. Wir betrachten den erweiterten Fall von solchen Sequenzen, in dem Zeit zwischen zwei verschiedenen Systemzuständen vergeht, und führen eine Logik ein, um solche Sequenzen zu beschreiben. Mit dieser Logik drücken wir zum einen Eigenschaften über die Struktur und die Attribute von Zuständen aus und beschreiben zum anderen temporale Vorkommen von Zuständen, die durch ihre innere Struktur verbunden sind. Solche Eigenschaften können bisher von keiner der existierenden Logiken auf Graphen vergleichbar darstellt werden. Erstens führen wir Graphen mit Änderungshistorie ein, indem wir jedes Graphelement mit einem Zeitstempel seiner Erzeugung und, wenn nötig, seiner Löschung versehen. Zweitens definieren wir eine Logik auf Graphen, indem wir den Temporaloperator Until in die wohl-etablierte Logik der verschachtelten Graphbedingungen integrieren. Drittens beweisen wir, dass unsere Logik gleich ausdrucksmächtig ist, wie die Logik der verschachtelten Graphbedingungen, indem wir eine passende Reduktionsoperation definieren. Zuletzt erlaubt uns die Implementierung dieser Reduktionsoperation die werkzeukbasierte Analyse von metrisch-temporallogischen Eigenschaften für Zustandssequenzen zu führen.
This will help us customize your experience to showcase the most relevant content to your age group
Please select from below
Login
Not registered?
Sign up
Already registered?
Success – Your message will goes here
We'd love to hear from you!
Thank you for visiting our website. Would you like to provide feedback on how we could improve your experience?
This site does not use any third party cookies with one exception — it uses cookies from Google to deliver its services and to analyze traffic.Learn More.