Input Synthesis for Sampled Data Systems by Program Logic
Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturbance or noise), find an input sequence that steers the system to the desired postcondition. In this paper we focus on sa...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2015-01-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1501.06005v1 |
id |
doaj-62f8c7b6564e4954b476bb20fa178e89 |
---|---|
record_format |
Article |
spelling |
doaj-62f8c7b6564e4954b476bb20fa178e892020-11-25T02:24:40ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-01-01174Proc. HAS 2014223910.4204/EPTCS.174.3:2Input Synthesis for Sampled Data Systems by Program LogicTakumi Akazaki0Ichiro Hasuo1Kohei Suenaga2 The University of Tokyo The University of Tokyo Kyoto University Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturbance or noise), find an input sequence that steers the system to the desired postcondition. In this paper we focus on sampled data systems—systems in which a digital controller interrupts a physical plant in a periodic manner, a class commonly known in control theory—and furthermore assume that a controller is given in the form of an imperative program. We develop a structural approach to input synthesis that features forward and backward reasoning in program logic for the purpose of reducing a search space. Although the examples we cover are limited both in size and in structure, experiments with a prototype implementation suggest potential of our program logic based approach.http://arxiv.org/pdf/1501.06005v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Takumi Akazaki Ichiro Hasuo Kohei Suenaga |
spellingShingle |
Takumi Akazaki Ichiro Hasuo Kohei Suenaga Input Synthesis for Sampled Data Systems by Program Logic Electronic Proceedings in Theoretical Computer Science |
author_facet |
Takumi Akazaki Ichiro Hasuo Kohei Suenaga |
author_sort |
Takumi Akazaki |
title |
Input Synthesis for Sampled Data Systems by Program Logic |
title_short |
Input Synthesis for Sampled Data Systems by Program Logic |
title_full |
Input Synthesis for Sampled Data Systems by Program Logic |
title_fullStr |
Input Synthesis for Sampled Data Systems by Program Logic |
title_full_unstemmed |
Input Synthesis for Sampled Data Systems by Program Logic |
title_sort |
input synthesis for sampled data systems by program logic |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2015-01-01 |
description |
Inspired by a concrete industry problem we consider the input synthesis problem for hybrid systems: given a hybrid system that is subject to input from outside (also called disturbance or noise), find an input sequence that steers the system to the desired postcondition. In this paper we focus on sampled data systems—systems in which a digital controller interrupts a physical plant in a periodic manner, a class commonly known in control theory—and furthermore assume that a controller is given in the form of an imperative program. We develop a structural approach to input synthesis that features forward and backward reasoning in program logic for the purpose of reducing a search space. Although the examples we cover are limited both in size and in structure, experiments with a prototype implementation suggest potential of our program logic based approach. |
url |
http://arxiv.org/pdf/1501.06005v1 |
work_keys_str_mv |
AT takumiakazaki inputsynthesisforsampleddatasystemsbyprogramlogic AT ichirohasuo inputsynthesisforsampleddatasystemsbyprogramlogic AT koheisuenaga inputsynthesisforsampleddatasystemsbyprogramlogic |
_version_ |
1724854214741458944 |