More Web Proxy on the site http://driver.im/

short-paper

Public Access

Compositional construction of bounded error over-approximations of acyclic interconnected continuous dynamical systems

Authors:

Pavithra PrabhakarAuthors Info & Claims

MEMOCODE '19: Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design

Article No.: 12, Pages 1 - 5

https://doi.org/10.1145/3359986.3361210

Published: 09 October 2019 Publication History

Abstract

We consider the problem of bounded time safety verification of interconnections of input-output continuous dynamical systems. We present a compositional framework for computing bounded error approximations of the complete system from those of the components. The main crux of our approach consists of capturing the input-output signal behaviors of a component using an abstraction predicate that represents the input-output sample behaviors corresponding to the signal behaviors. We define a semantics for the abstraction predicate that captures an over-approximation of the input-output signal behaviors of a component. Next, we define how to compose abstraction predicates of components to obtain an abstraction predicate for the composed system. We instantiate our compositional abstraction construction framework for linear dynamical systems by providing concrete methods for constructing the input-output abstraction predicates for the individual systems.

References

[1]

R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science.

[2]

R. Alur, T. Dang, and F. Ivancic. 2003. Counter-Example Guided Predicate Abstraction of Hybrid Systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

[3]

Rajeev Alur, Thao Dang, and Franjo Ivancic. 2006. Predicate abstraction for reachability analysis of hybrid systems. ACM Transactions on Embedded Computing Systems.

[4]

E. Asarin, T. Dang, and A. Girard. 2007. Hybridization methods for the analysis of nonlinear systems. Acta Informatica.

[5]

Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, and Dimitra Giannakopoulou. 2008. Automated Assume-Guarantee Reasoning by Abstraction Refinement. In International Conference on Computer Aided Verification.

Digital Library

[6]

Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina S. Pasareanu, Andreas Podelski, and Thomas Strump. 2014. Assume-Guarantee Abstraction Refinement Meets Hybrid Systems. In Haifa Verification Conference.

[7]

Xin Chen, Erika Abraham, and Sriram Sankaranarayanan. 2012. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In IEEE Real-Time Systems Symposium (RTSS).

[8]

Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, and Bow-Yaw Wang. 2010. Automated Assume-Guarantee Reasoning through Implicit Learning. In International Conference on Computer Aided Verification.

Digital Library

[9]

Chris Chilton, Bengt Jonsson, and Marta Z. Kwiatkowska. 2014. Compositional assume-guarantee reasoning for input/output component theories. Sci. Comput. Program.

[10]

A. Chutinan and B.H. Krogh. 2003. Computational techniques for hybrid system verification. IEEE Trans. Automat. Control.

[11]

E.M. Clarke, A. Fehnker, Z. Han, B. Krogh, J. Ouaknine, O. Stursberg, and M. Theobald. 2003. Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. Journal on Foundations of Computer Science.

[12]

T. Dang, O. Maler, and R. Testylier. 2010. Accurate hybridization of nonlinear systems. In International Conference on Hybrid Systems: Computation and Control.

[13]

Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In International Conference on Computer Aided Verification.

[14]

A. Girard. 2005. Reachability of uncertain linear systems using zonotopes. In International Conference on Hybrid Systems: Computation and Control.

Digital Library

[15]

Antoine Girard. 2013. A composition theorem for bisimulation functions. CoRR.

[16]

Antoine Girard and George J. Pappas. 2007. Approximation Metrics for Discrete and Continuous Systems. IEEE Trans. Automat. Contr.

[17]

T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya. 1995. What's decidable about hybrid automata?. In ACM Symposium on Theory of Computation.

[18]

Thomas A. Henzinger. 1996. The Theory of Hybrid Automata. In IEEE Symposium on Logic in Computer Science.

[19]

Ratan Lal and Pavithra Prabhakar. 2015. Bounded error flowpipe computation of parameterized linear systems. In International Conference on Embedded Software.

Digital Library

[20]

Ratan Lal and Pavithra Prabhakar. 2017. Safety analysis using compositional bounded error approximations of communicating hybrid systems. In Annual Conference on Decision and Control.

Digital Library

[21]

Alessio Lomuscio, Ben Strulo, Nigel G. Walker, and Peng Wu. 2013. Assume-Guarantee Reasoning with Local Specifications. Int. J. Found. Comput. Sci.

[22]

Nancy A. Lynch, Roberto Segala, and Frits W. Vaandrager. 2003. Hybrid I/O automata. Inf. Comput.

[23]

Wonhong Nam and Rajeev Alur. 2006. Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. In International Symposium on Automated Technology for Verification and Analysis.

[24]

André Platzer. 2011. Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial). In International Conference on Computer Aided Verification.

[25]

Pavithra Prabhakar and Mahesh Viswanathan. 2011. A dynamic algorithm for approximate flow computations. In International Conference on Hybrid Systems: Computation and Control.

Digital Library

[26]

Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. 2016. Hybridization Based CEGAR for Hybrid Automata with Affine Dynamics. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

[27]

Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. 2017. Robust Model Checking of Timed Automata under Clock Drifts. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Digital Library

[28]

Matthias Rungger and Majid Zamani. 2015. Compositional construction of approximate abstractions. In International Conference on Hybrid Systems: Computation and Control.

Digital Library

[29]

Paulo Tabuada, George J. Pappas, and Pedro U. Lima. 2004. Compositional Abstractions of Hybrid Control Systems. Discrete Event Dynamic Systems.

[30]

Yuichi Tazaki and Jun-ichi Imura. 2008. Bisimilar Finite Abstractions of Interconnected Systems. In International Conference on Hybrid Systems: Computation and Control.

[31]

Ashish Tiwari. 2008. Abstractions for hybrid systems. Formal Methods in System Design.

[32]

L. van den Dries and C. Miller. 1994. On the real exponential field with restricted analytic functions. Israel Journal of MAthematics.

Cited By

Alaoui SSaoud AJagtap PSwikir A(2023)Symbolic Models for Interconnected Impulsive Systems2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10383255(5900-5905)Online publication date: 13-Dec-2023
https://doi.org/10.1109/CDC49753.2023.10383255
Saoud AJagtap PZamani MGirard A(2021)Compositional Abstraction-Based Synthesis for Interconnected Systems: An Approximate Composition ApproachIEEE Transactions on Control of Network Systems10.1109/TCNS.2021.30501238:2(702-712)Online publication date: Jun-2021
https://doi.org/10.1109/TCNS.2021.3050123
Lal RMcKinnis AHauptman DKeshmiri SPrabhakar P(2021)Formally Verified Switching Logic for Recoverability of Aircraft ControllerComputer Aided Verification10.1007/978-3-030-81685-8_27(566-579)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_27
Show More Cited By

Index Terms

Compositional construction of bounded error over-approximations of acyclic interconnected continuous dynamical systems
1. General and reference
  1. Cross-computing tools and techniques
    1. Verification
2. Theory of computation
  1. Logic
    1. Abstraction
    2. Logic and verification

Recommendations

Verified systems by composition from verified components
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering

This paper presents an approach to integration of model checking into component-based development of software systems. This approach assists in development of highly reliable component-based software systems and reduces the complexity of verifying these ...
Verified systems by composition from verified components

This paper presents an approach to integration of model checking into component-based development of software systems. This approach assists in development of highly reliable component-based software systems and reduces the complexity of verifying these ...
Compositional Abstraction Refinement for Timed Systems
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering

Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MEMOCODE '19: Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design

October 2019

160 pages

ISBN:9781450369978

DOI:10.1145/3359986

General Chairs:
Partha Roop,
Naijun Zhan,
Program Chairs:
Sicun Gao,
Pierluigi Nuzzo

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

IEEE CAS
IEEE CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 October 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Funding Sources

Conference

MEMOCODE '19

Sponsor:

MEMOCODE '19: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design

October 9 - 11, 2019

California, La Jolla

Acceptance Rates

MEMOCODE '19 Paper Acceptance Rate 12 of 34 submissions, 35%;

Overall Acceptance Rate 34 of 82 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
231
Total Downloads

Downloads (Last 12 months)42
Downloads (Last 6 weeks)4

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Alaoui SSaoud AJagtap PSwikir A(2023)Symbolic Models for Interconnected Impulsive Systems2023 62nd IEEE Conference on Decision and Control (CDC)10.1109/CDC49753.2023.10383255(5900-5905)Online publication date: 13-Dec-2023
https://doi.org/10.1109/CDC49753.2023.10383255
Saoud AJagtap PZamani MGirard A(2021)Compositional Abstraction-Based Synthesis for Interconnected Systems: An Approximate Composition ApproachIEEE Transactions on Control of Network Systems10.1109/TCNS.2021.30501238:2(702-712)Online publication date: Jun-2021
https://doi.org/10.1109/TCNS.2021.3050123
Lal RMcKinnis AHauptman DKeshmiri SPrabhakar P(2021)Formally Verified Switching Logic for Recoverability of Aircraft ControllerComputer Aided Verification10.1007/978-3-030-81685-8_27(566-579)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81685-8_27
Ezudheen PAfzal ZPrabhakar PD’Souza DD’Souza M(2020)Verifying Band Convergence for Sampled Control SystemsNASA Formal Methods10.1007/978-3-030-55754-6_19(329-349)Online publication date: 11-May-2020
https://dl.acm.org/doi/10.1007/978-3-030-55754-6_19

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents