Tue 17 Jun 2014, 13:00-14:00
Georgios Fainekos (Arizona State University),
Temporal Logic Testing and Verification for Cyber-Physical Systems
理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7
アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)
One of the important challenges in the Model Based Development (MBD) of Cyber-Physical Systems (CPS) is the problem of verifying functional system properties. In its general form, the verification problem is undecidable due to the interplay between continuous and discrete system dynamics. In this talk, we present the bounded-time temporal logic testing and verification problem for CPS. Temporal logics can formally capture both state-space and real-time system requirements. For example, temporal logics can mathematically state requirements like "whenever the system switches to first gear, then it should not switch back to second gear within 2.5sec". Our approach in tackling this challenging problem is to convert the verification problem into an optimization problem through a notion of robustness for temporal logics. The robust interpretation of a temporal logic specification over a CPS trajectory quantifies "how much" the system trajectory satisfies or does not satisfy the specification. In general, the resulting optimization problem is non-convex and non-linear, the utility function is not known is closed-form and the search space is uncountable. Thus, stochastic search techniques are employed in order to solve the resulting optimization problem. We have implemented our testing and verification framework into a Matlab (TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). In this talk, we demonstrate that S-TaLiRo can provide answers to challenge problems from the automotive and medical device industries.
Georgios Fainekos is an Assistant Professor at the School of Computing, Informatics and Decision Systems (SCIDSE) Engineering at Arizona State University (ASU). He is director of the Cyber-Physical Systems Lab and he is currently affiliated with the Center for Embedded Systems at ASU. He received his Ph.D. in Computer and Information Science from the University of Pennsylvania in 2008 where he was affiliated with the GRASP laboratory. He holds a Diploma degree (B.Sc. & M.Sc.) in Mechanical Engineering from the National Technical University of Athens and an M.Sc. degree in Computer and Information Science from the University of Pennsylvania. Before joining ASU he held a Postdoctoral Researcher position at NEC Laboratories America in the System Analysis & Verification Group. He is currently working in the area of Cyber-Physical Systems (CPS) with focus on formal methods, logic, optimization and control theory with applications to automotive systems, autonomous (ground and aerial) robots and human-robot interaction (HRI). In 2014, Dr. Fainekos received the NSF CAREER award. He was recipient of the 2008 Frank Anger Memorial ACM SIGBED/SIGSOFT Student Award, and the 2013 Best Researcher Junior Faculty award from SCIDSE.
Wed 18 Jun 2014, 16:30-18:00
Liang-Ting Chen (Academia Sinica),
On a Categorical Framework for Coalgebraic Modal Logic
理学部7号館1階 102教室 Room 102, School of Science Bldg. No. 7
アクセス： https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html （一番下）
Access: http://www-mmm.is.s.u-tokyo.ac.jp/ (see bottom)
Two syntax-oriented approaches to coalgebraic modal logic — Moss’ cover modality and Pattinson’s predicate liftings — are successful in producing a wide range of modal logics parametric in a Set functor, including modal logics for Kripke frames, Markov chains, Markov processes, and their variants. Both of them can be presented abstractly in a form similar to mathematical SOS by Turi and Plokin, but this line of research was not well-understood yet.
In this talk I will treat the abstract formation seriously, and introduce a category of abstract semantics parametric in a contravariant functor that assigns to the state space its collection of predicates with propositional connectives. Various classical notions are formulated categorically. For example, modular constructions are identified as colimits, limits, and compositions of one-step semantics. The compositions and the colimits of (one-step) expressiveness semantics remain (one-step) expressive. In addition, we investigate a canonically-defined logic by its fibres, and show that it is a terminal object for every fibre.
By its very formulation, it is straightforward to show above results in this level of generality. In fact, I would like to suggest that it is the right level of abstraction for understanding coalgebraic modal logic. For further details, please see my MFPS paper, available in
http://www.cs.cornell.edu/Conferences/MFPS30/MFPS30-prelim.pdf