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...

Full description

Bibliographic Details
Main Authors: Takumi Akazaki, Ichiro Hasuo, Kohei Suenaga
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