LIAMA Shanghai Open Day 2013
Location: Room 113, Mathematics Building (In the North Zhongshan campus of East China Normal University)
Date: April 28, 2013
地址： 数学馆 113室（华东师范大学中山北路校区）（华东师范大学中山北路校区）
时间： 2013年4月28日 8:30-16:30
Registration Time: 8:30-8:55
Registration Location: Room 113, Mathematics Building (In the North Zhongshan campus of East China Normal University)
注册地点： 数学馆 113室（华东师范大学中山北路校区）
|08:55-09:00 Welcome Words
Prof. Yixiang Chen (Director of MOE Research Center for Software/Hardware Co-design Engineering)
(5-10 minutes for discussion are included in the presentations)
Session Chair: Prof. Robert De Simone (INRIA-Sophia Antipolis)
09:00-09:45 Prof. Jifeng He (Academician of Chinese Academy of Sciences, Dean of Software Engineering Institute, ECNU)
09:45-10:00 Coffee Break
10:00-11:40 Open Ceremony of LIAMA Shanghai Center
11:40-13:30 Lunch (Yifu Building)
Session Chair： Prof. Eric Madelaine
13:30-14:10 Prof. Yuxi Fu (Dean of School of Software Engineering, SJTU)
Title: "Checking Equality and Regularity for Normed BPA with Silent Moves”
Abstract: The decidability of weak bisimilarity on normed BPA is a long standing open problem. It is proved in this paper that branching bisimilarity, a standard refinement of weak bisimilarity, is decidable for normed BPA and that the associated regularity problem is also decidable.
14:10-14:50 Prof. Huibiao Zhu (Vice Director of Shanghai Key Laboratory of Trustworthy Computing)
Title: "Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language”
Abstract: Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. ), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper considers the link between the operational semantics and algebraic semantics for PTSC. Our investigation includes both the theoretical and practical approaches to the link.
In this talk, for aiming the link, we consider the inverse work, the derivation of operational semantics from algebraic semantics for our probabilistic language. This approach can be understood as the soundness investigation of operational semantics from the viewpoint of algebraic semantics. Firstly we present the algebraic laws for our probabilistic language. Every program can be expressed as either a guarded choice, or the summation of a set of processes which are deterministic initially. Secondly we investigate the derivation of an operational semantics from its algebraic semantics. Aset of transition rules are derived from the given derivation strategy. Thirdly we explore the equivalence of the derived transition system and the derivation strategy. This indicates the completeness of our operational semantics from the viewpoint of algebraic semantics. Besides the above theoretical approach to the link, we also study the practical approach to the link. We consider the animation of the link between operational semantics and algebraic semantics for PTSC.
14:50-15:10 Prof. Robert De Simone (Director AOSTE, INRIA-Sophia Antipolis)
Title: "Adequation Algorithm - Architecture for embedded systems”
15:10-15:30 Coffee Break
Session Chair: Prof. Yuxi Fu
15:30-15:50 Prof. Eric Madelaine (Director of OASIS, INRIA Sophia Antipolis)
Title: "Designing, programming, and verifying distributed systems "
15:50-16:30 Associate scientist Ludovic Henrio （INRIA Sophia Antipolis）
Title: “Formal Models for Programming and Composing Correct Distributed Systems”
16:30-16:50 Jianwen Li Ph.D student (Software Engineering Institute, ECNU)
Title: “On the Relationship between LTL Normal Forms and Büchi Automata”
Abstract: we revisit the problem of translating LTL formulas to Büchi automata. We first translate the given LTL formula into a special disjunctive-normal form (DNF). The formula will be part of the state, and its DNF normal form specifies the atomic properties that should hold immediately (labels of the transitions) and the formula that should hold afterwards (the corresponding successor state). If the given formula is Until-free or Release-free, the Büchi automaton can be obtained directly in this manner. For a general formula, the construction is slightly involved: an additional component will be needed for each formula that helps us to identify the set of accepting states. Notably, our construction is an on-the-fly construction, which starts with the given formula and explores successor states according to the normal forms. We implement our construction and compare the tool with SPOT. The comparison results are very encouraging and show our construction is quite innovative.
17:00-18:30 Dinner （Yifu Building）