Joint optimization and reachability analysis in graph transformation systems with time

Szilvia Gyapay, Ákos Schmidt, D. Varró

Research output: Contribution to journalArticle

15 Citations (Scopus)

Abstract

The design of safety critical systems frequently necessitates to simultaneously fulfill several logical and numerical constraints as requirements in order to deliver a functionally correct and optimal target system. In the current paper, we present a combined optimization and reachability analysis approach using the SPIN model checker [5] for problems modeled with graph transformation systems with time [3]. First, we encode graph transformation rules into transitions systems in Promela (the input language of SPIN) following [9,10]. Then we restrict valid execution paths to time-ordered transformation sequences by additional logical conditions. The desired reachability property (as logical condition) is used to potentially decrease the global best cost variable whenever a new path satisfies the property. The optimal solution for the problem is found by a single exhaustive run of the model checker encoding the numerical constraints into a dynamic LTL formula to cut off suboptimal paths violating the Branch-and-Bound heuristics.

Original languageEnglish
Pages (from-to)137-147
Number of pages11
JournalElectronic Notes in Theoretical Computer Science
Volume109
Issue number1-4 SPEC. ISS.
DOIs
Publication statusPublished - Dec 14 2004

Fingerprint

Reachability Analysis
Graph Transformation
Path
Optimization
Safety-critical Systems
Transition Systems
Spin Models
Branch-and-bound
Reachability
Encoding
Optimal Solution
Heuristics
Valid
Costs
Decrease
Target
Requirements
Model

Keywords

  • Graph transformation
  • Model checking
  • Optimization

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Joint optimization and reachability analysis in graph transformation systems with time. / Gyapay, Szilvia; Schmidt, Ákos; Varró, D.

In: Electronic Notes in Theoretical Computer Science, Vol. 109, No. 1-4 SPEC. ISS., 14.12.2004, p. 137-147.

Research output: Contribution to journalArticle

@article{059cbb64f61b45d0a887a42c83f701bb,
title = "Joint optimization and reachability analysis in graph transformation systems with time",
abstract = "The design of safety critical systems frequently necessitates to simultaneously fulfill several logical and numerical constraints as requirements in order to deliver a functionally correct and optimal target system. In the current paper, we present a combined optimization and reachability analysis approach using the SPIN model checker [5] for problems modeled with graph transformation systems with time [3]. First, we encode graph transformation rules into transitions systems in Promela (the input language of SPIN) following [9,10]. Then we restrict valid execution paths to time-ordered transformation sequences by additional logical conditions. The desired reachability property (as logical condition) is used to potentially decrease the global best cost variable whenever a new path satisfies the property. The optimal solution for the problem is found by a single exhaustive run of the model checker encoding the numerical constraints into a dynamic LTL formula to cut off suboptimal paths violating the Branch-and-Bound heuristics.",
keywords = "Graph transformation, Model checking, Optimization",
author = "Szilvia Gyapay and {\'A}kos Schmidt and D. Varr{\'o}",
year = "2004",
month = "12",
day = "14",
doi = "10.1016/j.entcs.2004.02.062",
language = "English",
volume = "109",
pages = "137--147",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "1-4 SPEC. ISS.",

}

TY - JOUR

T1 - Joint optimization and reachability analysis in graph transformation systems with time

AU - Gyapay, Szilvia

AU - Schmidt, Ákos

AU - Varró, D.

PY - 2004/12/14

Y1 - 2004/12/14

N2 - The design of safety critical systems frequently necessitates to simultaneously fulfill several logical and numerical constraints as requirements in order to deliver a functionally correct and optimal target system. In the current paper, we present a combined optimization and reachability analysis approach using the SPIN model checker [5] for problems modeled with graph transformation systems with time [3]. First, we encode graph transformation rules into transitions systems in Promela (the input language of SPIN) following [9,10]. Then we restrict valid execution paths to time-ordered transformation sequences by additional logical conditions. The desired reachability property (as logical condition) is used to potentially decrease the global best cost variable whenever a new path satisfies the property. The optimal solution for the problem is found by a single exhaustive run of the model checker encoding the numerical constraints into a dynamic LTL formula to cut off suboptimal paths violating the Branch-and-Bound heuristics.

AB - The design of safety critical systems frequently necessitates to simultaneously fulfill several logical and numerical constraints as requirements in order to deliver a functionally correct and optimal target system. In the current paper, we present a combined optimization and reachability analysis approach using the SPIN model checker [5] for problems modeled with graph transformation systems with time [3]. First, we encode graph transformation rules into transitions systems in Promela (the input language of SPIN) following [9,10]. Then we restrict valid execution paths to time-ordered transformation sequences by additional logical conditions. The desired reachability property (as logical condition) is used to potentially decrease the global best cost variable whenever a new path satisfies the property. The optimal solution for the problem is found by a single exhaustive run of the model checker encoding the numerical constraints into a dynamic LTL formula to cut off suboptimal paths violating the Branch-and-Bound heuristics.

KW - Graph transformation

KW - Model checking

KW - Optimization

UR - http://www.scopus.com/inward/record.url?scp=10444290082&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=10444290082&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2004.02.062

DO - 10.1016/j.entcs.2004.02.062

M3 - Article

VL - 109

SP - 137

EP - 147

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 1-4 SPEC. ISS.

ER -