Reasoning about linear systems

Rob Arthan; Ursula Martin; Erik Arne Mathiesen; Paulo Oliva

Reasoning about linear systems

Rob Arthan, Ursula Martin, Erik Arne Mathiesen, Paulo Oliva

School of Informatics

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

Abstract

We consider reasoning about linear systems expressed as block diagrams in a general relational setting. Using the notion of additive relation borrowed from homological algebra, the theory of weakest pre-conditions for these systems turns out to be very tractable and gives simple Hoarestyle rules for the block diagram constructors. Many natural choices for the logical language used to express properties of linear systems admit a high degree of automation. We show by example how the rules can be used to inform development of a proof while a decision procedure automates the routine work.

Original language	English
Title of host publication	Proceedings of 5th IEEE International Conference on Software Engineering and Formal Methods SEFM
Pages	123-134
Number of pages	10
Publication status	Published - 2007
Event	IEEE International Conference on Software Engineering and Formal Methods 2007 - London, United Kingdom Duration: 10 Sept 2007 → 14 Sept 2007

Conference

Conference	IEEE International Conference on Software Engineering and Formal Methods 2007
Abbreviated title	SEFM 2007
Country/Territory	United Kingdom
City	London
Period	10/09/07 → 14/09/07

Cite this

@inproceedings{27bc7c45deb5434592e71801aea4222e,

title = "Reasoning about linear systems",

abstract = "We consider reasoning about linear systems expressed as block diagrams in a general relational setting. Using the notion of additive relation borrowed from homological algebra, the theory of weakest pre-conditions for these systems turns out to be very tractable and gives simple Hoarestyle rules for the block diagram constructors. Many natural choices for the logical language used to express properties of linear systems admit a high degree of automation. We show by example how the rules can be used to inform development of a proof while a decision procedure automates the routine work.",

author = "Rob Arthan and Ursula Martin and Mathiesen, {Erik Arne} and Paulo Oliva",

year = "2007",

language = "English",

pages = "123--134",

booktitle = "Proceedings of 5th IEEE International Conference on Software Engineering and Formal Methods SEFM",

note = "IEEE International Conference on Software Engineering and Formal Methods 2007, SEFM 2007 ; Conference date: 10-09-2007 Through 14-09-2007",

}

TY - GEN

T1 - Reasoning about linear systems

AU - Arthan, Rob

AU - Martin, Ursula

AU - Mathiesen, Erik Arne

AU - Oliva, Paulo

PY - 2007

Y1 - 2007

N2 - We consider reasoning about linear systems expressed as block diagrams in a general relational setting. Using the notion of additive relation borrowed from homological algebra, the theory of weakest pre-conditions for these systems turns out to be very tractable and gives simple Hoarestyle rules for the block diagram constructors. Many natural choices for the logical language used to express properties of linear systems admit a high degree of automation. We show by example how the rules can be used to inform development of a proof while a decision procedure automates the routine work.

AB - We consider reasoning about linear systems expressed as block diagrams in a general relational setting. Using the notion of additive relation borrowed from homological algebra, the theory of weakest pre-conditions for these systems turns out to be very tractable and gives simple Hoarestyle rules for the block diagram constructors. Many natural choices for the logical language used to express properties of linear systems admit a high degree of automation. We show by example how the rules can be used to inform development of a proof while a decision procedure automates the routine work.

UR - https://www.eecs.qmul.ac.uk/~pbo/papers/paper015.pdf

M3 - Conference contribution

SP - 123

EP - 134

BT - Proceedings of 5th IEEE International Conference on Software Engineering and Formal Methods SEFM

T2 - IEEE International Conference on Software Engineering and Formal Methods 2007

Y2 - 10 September 2007 through 14 September 2007

ER -

Reasoning about linear systems

Abstract

Conference

Other files and links

Fingerprint

Cite this