Distributed lyapunov functions in analysis of graph models of software

Mardavij Roozbehani; Alexandre Megretski; Emilio Frazzoli; Eric Feron

doi:10.1007/978-3-540-78929-1_32

Distributed lyapunov functions in analysis of graph models of software

Mardavij Roozbehani, Alexandre Megretski, Emilio Frazzoli, Eric Feron

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

9 Scopus citations

Abstract

In previous works, the authors introduced a framework for software analysis, which is basedon optimization of Lyapunov invariants. These invariants prove critical software properties suchas absence of overflow and termination in finite time. In this paper, graph models of softwareare introduced and the software analysis framework is further developed and extended on graphmodels. A distributed Lyapunov function is assigned to the software by assigning a Lyapunovfunction to every node on its graph model. The global decremental condition is then enforced byrequiring that the Lyapunov functions on each node decrease as transitions take place along thearcs. The concept of graph reduction and optimality of graphs for Lyapunov analysis is brieflydiscussed. © 2008 Springer-Verlag Berlin Heidelberg.

Original language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer Verlag
Pages	443-456
Number of pages	14
ISBN (Print)	3540789286
DOIs	https://doi.org/10.1007/978-3-540-78929-1_32
State	Published - Jan 1 2008
Externally published	Yes

Bibliographical note

Generated from Scopus record by KAUST IRTS on 2021-02-18

Access to Document

10.1007/978-3-540-78929-1_32

Cite this

@inproceedings{913d518fb8474ca29db7895968c95289,

title = "Distributed lyapunov functions in analysis of graph models of software",

abstract = "In previous works, the authors introduced a framework for software analysis, which is basedon optimization of Lyapunov invariants. These invariants prove critical software properties suchas absence of overflow and termination in finite time. In this paper, graph models of softwareare introduced and the software analysis framework is further developed and extended on graphmodels. A distributed Lyapunov function is assigned to the software by assigning a Lyapunovfunction to every node on its graph model. The global decremental condition is then enforced byrequiring that the Lyapunov functions on each node decrease as transitions take place along thearcs. The concept of graph reduction and optimality of graphs for Lyapunov analysis is brieflydiscussed. {\textcopyright} 2008 Springer-Verlag Berlin Heidelberg.",

author = "Mardavij Roozbehani and Alexandre Megretski and Emilio Frazzoli and Eric Feron",

note = "Generated from Scopus record by KAUST IRTS on 2021-02-18",

year = "2008",

month = jan,

day = "1",

doi = "10.1007/978-3-540-78929-1_32",

language = "English (US)",

isbn = "3540789286",

pages = "443--456",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

address = "Germany",

}

Distributed lyapunov functions in analysis of graph models of software. / Roozbehani, Mardavij; Megretski, Alexandre; Frazzoli, Emilio et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, 2008. p. 443-456.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Distributed lyapunov functions in analysis of graph models of software

AU - Roozbehani, Mardavij

AU - Megretski, Alexandre

AU - Frazzoli, Emilio

AU - Feron, Eric

N1 - Generated from Scopus record by KAUST IRTS on 2021-02-18

PY - 2008/1/1

Y1 - 2008/1/1

N2 - In previous works, the authors introduced a framework for software analysis, which is basedon optimization of Lyapunov invariants. These invariants prove critical software properties suchas absence of overflow and termination in finite time. In this paper, graph models of softwareare introduced and the software analysis framework is further developed and extended on graphmodels. A distributed Lyapunov function is assigned to the software by assigning a Lyapunovfunction to every node on its graph model. The global decremental condition is then enforced byrequiring that the Lyapunov functions on each node decrease as transitions take place along thearcs. The concept of graph reduction and optimality of graphs for Lyapunov analysis is brieflydiscussed. © 2008 Springer-Verlag Berlin Heidelberg.

AB - In previous works, the authors introduced a framework for software analysis, which is basedon optimization of Lyapunov invariants. These invariants prove critical software properties suchas absence of overflow and termination in finite time. In this paper, graph models of softwareare introduced and the software analysis framework is further developed and extended on graphmodels. A distributed Lyapunov function is assigned to the software by assigning a Lyapunovfunction to every node on its graph model. The global decremental condition is then enforced byrequiring that the Lyapunov functions on each node decrease as transitions take place along thearcs. The concept of graph reduction and optimality of graphs for Lyapunov analysis is brieflydiscussed. © 2008 Springer-Verlag Berlin Heidelberg.

UR - http://link.springer.com/10.1007/978-3-540-78929-1_32

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

U2 - 10.1007/978-3-540-78929-1_32

DO - 10.1007/978-3-540-78929-1_32

M3 - Conference contribution

SN - 3540789286

SP - 443

EP - 456

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -

Distributed lyapunov functions in analysis of graph models of software

Abstract

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this