ROSAEC center Seoul National University
NRF

Seminars & Workshops

Speaker:Kyungmin Bae , Univ. of Illinois at Urbana-Champaign
When:2010-01-05 15:00
Place:Room 309-1, Bldg 302, SNU

Abstract

The Linear Temporal Logic of Rewriting (LTLR) extends linear temporal logic with spatial action patterns which represent properties related to events. LTLR generalizes and extends various state-based and event-based logics and aims to avoid certain types of mismatches between a system and its temporal logic properties. We have implemented the LTLR model checker within the Maude system by extending the existing Maude LTL model checker. Our LTLR model checker provides very expressive methods to define event-related properties as well as state-related properties, or more generally properties involving both event and state predicates. This greater expressiveness is gained without compromising performance, because the LTLR implementation minimizes the extra costs involved in handling the events of systems.

Short bio

Kyungmin is a Ph.D. candidate in Computer Science, UIUC.

Resources



© Copyright 2008-2010 ROSAEC Center, Seoul National University