Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 2/2013

01-04-2013

An approximation algorithm for box abstraction of transition systems on real state spaces

Authors: Kunihiko Hiraishi, Koich Kobayashi

Published in: Formal Methods in System Design | Issue 2/2013

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Predicate abstraction is a powerful technique for extracting finite-state models from infinite-state systems such as computer software, and is applied to verification of safety properties. Predicate abstraction is also applied to verification of dynamical systems on real state spaces such as hybrid dynamical systems. In this paper, we propose a fast algorithm for computing entire abstract state spaces of transition systems on real state spaces. The method is based on the box abstraction of state spaces, and requires a relatively smaller number of reachability checks and Boolean operations. We also propose a fast method for computing the set of boxes that intersect a given convex polyhedron. This computation is a part of the proposed state-space generation algorithm. Effectiveness of the algorithm is evaluated by the computation time and by the difference of the approximated state space from the exact state space.
previous article Code aware resource management
next article Weighted modal transition systems

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Literature
1.
2.
Guèhuen H, Lefebvre M, Zaytoon J, Nasri O (2009) Safety verification and reachability analysis for hybrid systems. Annu Rev Control 33:25–36 CrossRef
3.
Alur R, Henzinger TA, Ho P-H (1996) Automatic symbolic verification of embedded systems. IEEE Trans Softw Eng 22:181–201 CrossRef
4.
Larsen KG, Petterson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1–2):134–152 MATHCrossRef
5.
Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transf 1(1–2):123–133 MATHCrossRef
6.
Bjørner N, Manna Z, Sipma H, Utribe T (1997) Deductive verification of real-time systems using STeP. In: Proc international AMAST workshop in real-time systems. Lecture notes in computer science, vol 1231, pp 22–43
7.
Chutinan A, Krough BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64–75 CrossRef
8.
Asarin E, Bournez O, Dang T, Maler O (2000) Approximate reachability analysis of piecewise linear dynamical systems. In: Proc 3rd int workshop on hybrid systems: computation and control. Lecture notes in computer science, vol 1790, pp 21–31
9.
Alur R, Henzinger TA, Lafferriwre G, Pappas GJ (2000) Discrete abstraction of hybrid systems. Proc IEEE 88(7):971–984 CrossRef
10.
Alur R, Dang T, Ivanc̆ić F (2002) In: Reachability analysis of hybrid systems via predicate abstraction 5th international workshop on hybrid systems: computation and control. Lecture note in computer science, vol 2289, pp 35–48 CrossRef
11.
Alur R, Dang T, Ivanc̆ić F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354:250–271 MATHCrossRef
12.
Geyer T, Torrisi FD, Morari M (2004) Optimal complexity reduction of piecewise affine models based on hyperplane arrangement. In: Proc 2004 American control conference, pp 1190–1195
13.
Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Transactions on Embedded Computing Systems 6(1): Article No. 8
14.
Clarke EM Jr., Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge
15.
16.
De Loera JA, Hemmecke R, Tauzer J, Yoshida R (2003) Effective lattice point counting in rational convex polytopes. J Symb Comput 38:1273–1302 CrossRef
17.
Hertel S, Mäntylä M, Mehlhorn K, Nievergelt J (1984) Space sweep solves intersection of convex polyhedra. Acta Inform 21:501–519 MathSciNetMATHCrossRef
18.
19.
20.
Hiraishi K (2006) KCLP-HS: a rapid prototyping tool for implementing algorithms on hybrid systems. JAIST research report IS-RR-2006-012
Metadata
Title
An approximation algorithm for box abstraction of transition systems on real state spaces
Authors
Kunihiko Hiraishi
Koich Kobayashi
Publication date
01-04-2013
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 2/2013
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0175-z

Premium Partner

    Image Credits