Infinite-state graph transformation systems under adverse conditions

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Okan Özkan
Keyword(s):  
Model Checking ◽  
Graph Transformation ◽  
State Graph ◽  
State Spaces ◽  
Adverse Conditions ◽  
Computation Tree ◽  
Temporal Model ◽  
Transformation Systems ◽  
Graph Transformation Systems ◽  
Infinite State

Abstract We present an approach for modeling adverse conditions by graph transformation systems. To this end, we introduce joint graph transformation systems which involve a system, an interfering environment, and an automaton modeling their interaction. For joint graph transformation systems, we present notions of correctness under adverse conditions. Some instances of correctness are expressible in LTL (linear temporal logic), or in CTL (computation tree logic), respectively. In these cases, verification of joint graph transformation systems is reduced to temporal model checking. To handle infinite state spaces, we incorporate the concept of well-structuredness. We discuss ideas for the verification of joint graph transformation systems using results based on well-structuredness.

scholarly journals Compositional Analysis of Probabilistic Timed Graph Transformation Systems

2021 ◽  
pp. 196-217
Author(s):  
Maria Maximova ◽  
Sven Schneider ◽  
Holger Giese
Keyword(s):  
Large Scale ◽  
Graph Transformation ◽  
Mutual Exclusion ◽  
Compositional Analysis ◽  
Behavioral Models ◽  
State Spaces ◽  
Large Scale System ◽  
Qualitative And Quantitative ◽  
Transformation Systems ◽  
Graph Transformation Systems

AbstractThe analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on e.g. concurrent components with mutual exclusion or probabilistic failures on demand. The rule-based formalism of probabilistic timed graph transformation systems is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces.We present an approach for the analysis of large-scale systems modeled as probabilistic timed graph transformation systems by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large-scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large-scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large-scale system under analysis. We consider a running example in which we model shuttles driving on tracks of a large-scale topology and for which we verify that shuttles never collide and are unlikely to execute emergency brakes. In our evaluation, we apply an implementation of our approach to the running example.

Sign in / Sign up

Export Citation Format

Share Document