主催：NII 先端ソフトウェア工学国際研究センター（GRACEセンター）
http://grace-center.jp/
日時：2010年4月22日（木）10:00-12:00
場所：国立情報学研究所(NII) 20階講義室1(2005) （地図）
参加費：無料
お問い合わせ：加藤 弘之 (kato_AT_nii.ac.jp)_AT_を＠に書き換えてください。
参加をご希望の方は、セミナー前日までに下記よりご登録をお願いします。
http://grace-center.jp/regist/seminar
===================================================
Details:
FIRST SPEAKER
Eric Platon (National Institute of Informatics)
=== Title ===
Software Engineering Practices: Update at the Source from a Startup
=== Abstract ===
Industry and academic research have sometimes quite different views on
Software Engineering practices, except perhaps the common goal to
build software that works. Most advances in engineering however result
from interactions between industry and research. The cooperation
typically examines how to apply general research results in specific
cases raised in industrial activities, or how to solve a new problem,
first in any possible way.
In this talk, I will rely on two years recently spent in a Japanese
startup to present some success and failure in applying research
results in practice, and to express some needs. This presentation will
range from the formulation of requirements, to development hygiene, to
testing and verification, and some other aspects.
Despite the idiosyncrasy of the cases at hand, I believe that several
of these problems are recurrent in industry, with informal
confirmation from partner companies and research institutes.
Research groups on Software Engineering can readily provide solutions
to some of these issues, but cooperation, education, and discipline
seem the most beneficial practical targets one should pursue, together
with feeding researchers with concrete needs.
===================================================
Details:
SECOND SPEAKER
Yoshinori Tanabe (National Institute of Informatics)
=== Title ===
A natural number-valued semantics of the modal mu-calculus.
=== Abstract ===
The modal mu-calculus is an extension of the modal logic K with
fixed-point operators, which give the logic strong expressive
power: it is possible to express, for example, reachability properties
and orders among events with simple formulas. Model-checking
algorithms and decision procedures for the satisfiability problem of
the logic have been widely investigated, and they have various
applications.
We define a semantics of the logic based on min-plus algebra
N-infinity. N-infinity is the set of all natural numbers and
infinity, and has two operations min and plus. In the semantics,
disjunctions are interpreted by the min operator and conjunctions by
the plus operator. This semantics allows interesting properties of
graphs, such as the shortest path to some state or the number of
states that satisfy a specified condition, to be expressed using
simple formulae.
In this talk, we discuss model checking algorithms and decision
procedures for the satisfiability problem of the logic with the
N-infinity semantics. The former gives a procedure to calculate the
values of functions from a graph to N-infinity defined in terms of
fixed-point operations. The latter will enable us to reason about the
statements referring to such functions.
