14:00 - 18:00 REGISTRATION
19:00 - 21:30 RECEPTION


8:00 - 9:00 REGISTRATION
9:00 - 9:30 OPENING SEESION (Chair: Danning Li, Guizhou Academy of Sciences, China)
  Welcome Speech
Someone from the local organization

About UNU-IIST: Jifeng He, UNU-IIST, Macao

Report on the Work of the Program Committee
Zhiming Liu, PC Co-chair of ICTAC 2004, UNU-IIST, Macao
9:30 - 10:30 KEYNOTE TALK 1 (Chair: Keijiro Araki, Kyushu University, Japan)
  Jifeng He, UNU-IIST, Macao
10:30 - 11:00 BREAK
11:00 - 13:00 SESSION 1A: AUTOMATA THEORY AND LOGICS (Chair: Huimin Lin, Institute of Software, Chinese Academy of Sciences, China)
  Reasoning about co-Büchi Tree Automata
Salvatore La Torre and Aniello Murano (Università degli Studi di Salerno, Italy)

Switched Probabilistic I/O Automata
Ling Cheung, Frits Vaandrager (University of Nijmegen, The Netherlands), Nancy Lynch (MIT Computer Science and Artifical Intelligence Laboratory, USA) and Roberto Segala (Università di Verona, Italy)

Foundations for the Run-time Monitoring of Reactive Systems - Fundamentals of the MaC language
Mahesh Viswanathan (University of Illinois at Urbana Champaign, USA) and Moonzoo Kim (Pohang University of Science and Technology, Korea)

Duration Calculus: A Real-time Semantic for B
Samuel Colin, Georges Mariano (INRETS, France) and Vincent Poirriez (LAMIH, France)
11:00 - 13:00 SESSION 1B: REAL-TIME AND CO-DESIGN (Chair: Paddy Krishnan, Bond University, Australia)
  An Algebraic Approach for Codesign
Marc Aiguier, Stefan Béroff (Université d'Évry Val d'Essonne, France) and Pierre-Yves Schobbens (Institut d'Informatique, Belgium)

A Framework for Specification and Validation of Real-time Systems using Circus Actions
Adnan Sherif, Augusto Sampaio (CIn/UFPE, Brazil), He Jifeng (UNU-IIST, Macao) and Ana Cavalcante (University of Kent, UK)

A Calculus for Shapes in Time and Space
Andreas Schäefer (University of Oldenburg, Germany)

An Algebra of Petri Nets with Arc-based Time Restrictions
Apostolos Niaouris (University of Newcastle, UK)
13:00 - 14:30 LUNCH
14:30 - 15:30 KEYNOTE TALK 2 (Chair: K. Rustan M. Leino, Microsoft Research, USA)
  Jose Luiz Fiadeiro, University of Leicester, UK
15:30 - 16:00 BREAK
16:00 - 18:00 SECTION 2A: SYSTEM MODELLING AND APPLICATION OF LOGICS (Chair: Raymond Boute, Ghent University, Belgium)
  Atomic Components
Steve Reeves and David Streader (University of Waikato, New Zealand)

A Proof of Weak Termination Providing the Right Way to Terminate
Olivier Fissore, Isabelle Gnaedig and Hélène Kirchner (LORIA-INRIA & LORIA-CNRS, France)

A Logical Characterization of Efficiency Preorders
Neelesh Korade (Persistent Systems Private Limited, India) and S. Arun-Kumar (Indian Institute of Technology, India)

Specifying Software Connectors
Marco Antonio Barbosa and Luís Soares Barbosa (Universidade do Minho, Portugal)
16:00 - 18:00 SECTION 2B: DISTRIBUTED SYSTEMS (Chair: Jing Song Dong, National University, Singapore)
  A Static Analysis for Security Properties in PKI-based Protocols
Benjamin Aziz (University College Cork, Ireland), David Gray and Geoff Hamilton (Dublin City University, Ireland)

Decomposing Controllers into Non-conflicting Distributed Controllers
Padmanabhan Krishnan (Bond University, Australia)

Towards an Optimization-based Method for Consolidating Domain Variabilities in Domain-specific Web Services Composition
Jun-feng Zhao, Lu Zhang, Ya-sha Wang, Ying Jiang and Bing Xie (Peking University, China)

Replicative - Distribution Rules in P Systems with Active Membranes
Tseren-Onolt Ishdorj (The State University of Education of Mongolia, Mongolia) and Mihai Ionescu (Rovira i Virgili University, Spain)


8:30 - 9:30 KEYNOTE TALK 3 (Chair: Zhiming Liu, UNU-IIST, Macao)
  Huimin Lin, Institute of Software, Chinese Academy of Sciences, China
9:30 - 10:00 BREAK
10:00 - 12:00 SESSION 3A: AUTOMATED PROOF AND MODEL CHECKING (Chair: Ryszard Janicki, McMaster University, Canada)
  Idempotent Relations in Isabelle/HOL
Florian Kammüeller (Technische Universität Berlin, Germany) and J.W. Sanders (University of Oxford, UK)

Symbolic and Parametric Model Checking of Discrete-Time Markov Chains
Conrado Daws (University of Twente, The Netherlands)

Verifying Linear Duration Constraints of Timed Automata
Pham Hong Thai and Dang Van Hung (UNU-IIST, Macao)

Program Verification Using Automatic Generation of Invariants
Enric Rodríguez-Carbonell (Technical University of Catalonia, Spain) and Deepak Kapur (University of New Mexico, USA)
10:00 - 12:00 SESSION 3B: MODEL INTEGRATION AND TEHORY UNIFICATION (Chair: Shaoying Liu, Hosei University, Japan)
  A Formal Framework for Ontology Integration Based on a Default Extension to DDL
Yinglong Ma, Jun Wei and Shaohua Liu (Institute of Software, Chinese Academy of Sciences, China)

A Predicative Semantic Model for Integrating UML Models
Jing Yang, Quan Long (UNU-IIST, Macao) and Xiaoshan Li (University of Macau, Macao)

Automatic Mapping from Statecharts to Verilog
Viet-Anh Vu Tran (Vietsoftware Company, Vietnam), Shengchao Qin and Wei Ngan Chin (National University of Singapore, Singapore)

Reverse Observation Equivalence Between Labelled State Transition Systems
Yanjun Wen, Ji Wang and Zhichang Qi (National Laboratory for Parallel and Distributed Processing, China)
12:00 - 13:30 LUNCH
13:30 - 14:30 KEYNOTE TALK 4 (Chair: Jeff Sanders, Oxford University, UK)
  K. Rustan M. Leino, Microsoft Research, USA
14:30 - 15:00 BREAK
15:00 - 17:00 SESSION 4A: PROGRAM TESTING AND REASONING (Chair: Hong Zhu, Oxford Brookes University, UK)
  An Approach to Integration Testing Based on Data Flow Specifications
Yuting Chen, Shaoying Liu, and Fumiko Nagoya (Hosei University, Japan)

Combining Algebraic and Model-based Test Case Generation
Li Dan and Bernhard K. Aichernig (UNU-IIST, Macao)

Minimal Spanning Set for Coverage Testing of Interactive Systems
Fevzi Belli and Christof J. Budnik (University of Paderborn, Germany)

Reasoning about OWL & ORL Ontologies in PVS
Jin Song Dong, Yu Zhang Feng and Yuan Fang Li (National University of Singapore, Singapore)
15:00 - 17:00 SESSION 4B: THEORIES OF PROGRAMMING AND PROGRAMMING LANGUAGES (Chair: Hongjun Zheng, Semantics Designs Inc, USA)
  Random Generators for Dependent Types
Peter Dybjer, Qiao Haiyan (Chalmers University of Technology, Sweden) and Makoto Takeyama (National Institute of Advanced Industrial Science and Technology, Japan)

Real Time Reactive Programming in Lucid Enriched with Contexts
Kaiyu Wan, Vasu Alagar and Joey Paquet (Concordia University, Canada)

A New Correctness Proof for Positive Equality
Miroslav N. Velev (Carnegie Mellon University, USA)

Revision Programs with Explicit Negation
Yisong Wang (Guizhou University, China) and Zhang Mingyi (Guizhou Academy of Sciences, China)



8:30 - 10:30 SESSION 5: CONCURRENCY AND MODULARITY (Chair: José Luiz Fiadeiro, University of Leicester, UK)
  Inherent Causal Orderings of Partial Order Scenarios
Bill Mitchell (University of Surrey, UK)

A Generalisation of a Relational Structures Model of Concurrency
Ryszard Janicki (McMaster University, Canada)

Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn
Silvio Ranise, Christophe Ringeissen and Duc-Khanh Tran (LORIA-INRIA, France)

Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes
Erika Ábrahám (University Freiburg, Germany), Marcello M. Bonsangue (Univeristy Leiden, The Netherlands), Frank S. de Boer (CWI Amsterdam, The Netherlands) and Martin Steffen (Christian-Albrechts-University Kiel, Germany)
10:30 - 11:00 BREAK
11:00 - 11:30 CLOSING SESSION (Chair: Zhiming Liu, UNU-IIST, Macao)
11:30 - 13:00 LUNCH
13:00 - 20:00 EXCURSION