Ichiro Hasuo,
Associate
Professor
at
Department
of
Computer
Science,
the
University
of
Tokyo,
Japan
Talk
1:
"Lattice-theoretic
progress
measures
and
co-algebraic
model
checking"
Abstract:
In
the
context
of
formal
verification
in
general
and
model
checking
in
particular,
parity
games
serve
as
a
mighty
vehicle:
many
problems
are
encoded
as
parity
games,
which
are
then
solved
by
the
seminal
algorithm
by
Jurdzinski.
In
this
paper
we
identify
the
essence
of
this
workflow
to
be
the
notion
of
progress
measure,
and
formalize
it
in
general,
possibly
infinitary,
lattice-theoretic
terms.
Our
view
on
progress
measures
is
that
they
are
to
nested/alternating
fixed
points
what
invariants
are
to
safety/greatest
fixed
points,
and
what
ranking
functions
are
to
liveness/least
fixed
points.
That
is,
progress
measures
are
combination
of
the
latter
two
notions
(invariant
and
ranking
function)
that
have
been
extensively
studied
in
the
context
of
(program)
verification.
We
then
apply
our
theory
of
progress
measures
to
a
general
model-checking
framework,
where
systems
are
categorically
presented
as
coalgebras.
The
framework's
theoretical
robustness
is
witnessed
by
a
smooth
transfer
from
the
branching-time
setting
to
the
linear-time
one.
Although
the
framework
can
be
used
to
derive
some
decision
procedures
for
finite
settings,
we
also
expect
the
proposed
framework
to
form
a
basis
for
sound
proof
methods
for
some
undecidable/infinitary
problems.
(Based
on
the
joint
work
with
Shunsuke
Shimizu
and
Corina
Cirstea
presented
at
POPL
2016)
============================
Talk
2:
"Time
Robustness
in
MTL
and
Expressivity
in
Hybrid
System
Falsification"
Abstract:
Building
on
the
work
by
Fainekos
and
Pappas
and
the
one
by
Donze
and
Maler,
we
introduce
AvSTL,
an
extension
of
metric
interval
temporal
logic
by
averaged
temporal
operators.
Its
expressivity
in
capturing
both
space
and
time
robustness
helps
solving
falsification
problems,
(i.e.
searching
for
a
critical
path
in
hybrid
system
models);
it
does
so
by
communicating
a
designer's
intention
more
faithfully
to
the
stochastic
optimization
engine
employed
in
a
falsification
solver.
We
also
introduce
a
sliding
window-like
algorithm
that
keeps
the
cost
of
computing
truth/robustness
values
tractable.
(Based
on
the
joint
work
with
Takumi
Akazaki
presented
at
CAV
2015)
============================
Short
bio:
Ichiro Hasuo is
an
Associate
Professor
at
Department
of
Computer
Science,
the
University
of
Tokyo,
Japan,
and
is
the
research
director
of
the
JST
ERATO
"Metamathematics
for
Systems
Design"
Project.
He
received
PhD
(cum
laude)
in
Computer
Science
from
Radboud
University
Nijmegen,
the
Netherlands,
in
2008
where
he
was
affiliated
with
the
Security
of
Systems
group
and
supervized
by
Prof.Dr.
Bart
Jacobs.
Before
joining
UTokyo
he
held
an
Assistant
Professor
position
at
Research
Institute
for
Mathematical
Sciences
(RIMS),
Kyoto
University,
Japan.
His
research
interests
include:
mathematical
(logical,
algebraic
and
categorical)
structures
in
software
science
(esp.
formal
methods);
abstraction
and
generalization
of
deductive
and
automata-theoretic
verification
techniques;
and
their
application
to
cyber-physical
systems.
He
is
a
recipient
of:
Hiroshi
Fujiwara
Encouragement
Prize
for
Mathematical
Sciences
in
2012
(supported
by
Mathematical
Society
of
Japan);
the
best
paper
award
at
CONCUR
2014
(jointly
with
Natsuki
Urabe);
a
JST
PRESTO
researchership;
and
a
JST
ERATO
project
(three
were
granted
in
2016
out
of
proposals
from
all
scientific
fields).