Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016.
This volume contains the papers presented at CS&P 2016, the 25th International Workshop on Concurrency, Speciﬁcation and Programming, held on September 28 - 30, 2016 in Rostock, Germany. Since the early seventies Warsaw University and Humboldt University have alternately organized an annual workshop - since the early nineties known as CS&P. Over time, it has grown from a bilateral seminar to a well-known meeting attended also by colleagues from many other countries than Poland and Germany. This year marks an anniversary: we celebrate the quarter-centenary edition of CS&P. We do so on the Baltic Sea coast, in one of the oldest universities in the world, the University of Rostock, founded in 1419. The gathering is hosted by Rostock University’s department of computer science, and the editor would like to thank Prof. Karsten Wolf and his local team for their hospitality and great organization. During the three-day meeting, there are 14 sessions in two parallel tracks. Additionally, there is a number of short presentations on current and emerging topics, as well as tool demos and open discussions. This volume contains 26 papers supplementing the presentations, selected from the submissions by the program committee. Following the workshops tradition, we strive to retain an informal working atmosphere. Therefore, the proceedings includes drafts and extended abstracts as well as fully elaborated contributions. The proceedings are published by Humboldt University and CEUR. The editor would like to thank the university’s printing oﬃce, the team at CEUR Workshop Proceedings, and EasyChair for their help in producing this publication.
By sequential reactive system we mean a program which operates in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data a program performs a sequence of actions (response) and displays the current result. Such programs usually arise at implementation of computer drivers, online algorithms, control procedures. Basic actions performed by these programs may be regarded as generating elements of a certain semigroup. This consideration opens the way to model sequential reactive systems by ﬁnite state transducers that operate over semigroups. This model of computation is suitable for synthesis, optimization, veriﬁcation and testing of sequential reactive systems. In this paper we originate a framework for developing veriﬁcation techniques for sequential reactive systems by utilizing ﬁnite state transducers as a formal model. To this end we introduce a LTL-based formal language which may be suitable for speciﬁcation of the behaviour of sequential reactive systems and adopt a well known LTL-based model checking techniques for veriﬁcation of ﬁnite state transducers against these speciﬁcations.