[logic-ml] Talks at UTokyo: Georgios Fainekos (Tue 17), Liang-Ting Chen (Wed 18)

[Ichiro Hasuo]

Dear colleagues,

It is my pleasure to announce two talks given by visitors to
our group: Georgios Fainekos (tomorrow) on cyber-physical
systems; and Liang-Ting Chen (Wed) on categorical and coalgebraic
logic. No registration is needed; see you there!

Best regards,
Ichiro Hasuo

Group MMM, University of Tokyo
http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar


------------------------------

Tue 17 Jun 2014, 13:00-14:00

Georgios Fainekos <http://www.public.asu.edu/~gfaineko/> (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 <http://uk.linkedin.com/pub/liang-ting-chen/88/749/b5a>
(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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20140616/1243694d/attachment.html>