Stephane Le Roux is visiting

Stephane Le Roux is visiting us from Darmstadt. Today he will give a talk on “Concurrent games and semi-random determinacy.”

Abstract: Consider concurrent, infinite duration, two-player win/lose games played on graphs. If the winning condition satisfies some simple requirement, the existence of Player 1 winning (finite- memory) strategies is equivalent to the existence of winning (finite-memory) strategies in finitely many derived one-player games. Several classical winning conditions satisfy this simple requirement.Under an additional requirement on the winning condition, the non-existence of Player 1 winning strategies from all vertices is equivalent to the existence of Player 2 stochastic strategies almost-sure winning from all vertices. Only few classical winning conditions satisfy this additional requirement, but a fairness variant of omega-regular languages does.

Amir Tabatabai and Rahele Jalali visiting

Amir Tabatabai and Rahele Jalali, both PhD students at the Institute of Mathematics of the Czech Academy of Sciences under the supervision of Pavel Pudlak, are visiting Swansea University 13 Nov – 6 Dec 2017.

Amir will give a talk on Computational Flows in Arithmetic on 16 November.

More information: A computational flow is a pair consisting of a sequence of computational  problems of a certain sort and a sequence of computational reductions among
them. In this talk we will explain the basics of the theory of computational
flows and how they make a sound and complete interpretation for bounded
theories of arithmetic. This property helps us to decompose a first order
arithmetical proof to a sequence of computational reductions by which we can
extract the computational content of the low complexity statements in some
bounded theories of arithmetic such as  $I\Delta_0, T^k_n, I\Delta_0 + EXP \text{ and } PRA$.

Jan Peleska and Wen-ling Huang visiting

Jan Peleska and Wen-ling Huang from the University of Bremen are visiting Swansea this week. Jan will give a talk on Safety-complete Test Suites as a part of Computational Foundry Seminar series.

More information: This presentation is about property-oriented testing. A novel safety-related variant of complete test suites for ﬁnite state machines is introduced. Under certain hypotheses which are similar to the ones used in the well-known complete testing methods like W-Method, Wp-Method, HSI-Method, or H-Method, the new method guarantees to uncover every safety violation, while erroneous outputs without safety-relevance may remain undetected. In well-deﬁned situations that can be precisely pre-determined from the reference model, this leads to a substantial reduction of test cases in comparison to the size of the analogous W, WP, HSI, H-test suites. We advocate this new test strategy for situations, where exhaustive testing of the complete system is too expensive. In these cases, strong guarantees with respect to fault coverage should only be given for the errors representing safety violations, while it is considered as acceptable if less critical errors remain undetected. An original version of this material has been published at the ICTSS 2017 conference; in this talk, we present a refined test suite based on the H-method which can be shown to always produce less or equally many test cases as when applying the original H-method. We sketch how this strategy can be extended to safety-complete equivalence class testing for systems with infinite input domains but finitely many internal states and finite output domains.