Sciweavers

CONCUR
2000
Springer
14 years 2 months ago
Model Checking with Finite Complete Prefixes Is PSPACE-Complete
Unfoldings are a technique for verification of concurrent and distributed systems introduced by McMillan. The method constructs a finite complete prefix, which can be seen as a sym...
Keijo Heljanko
CONCUR
2000
Springer
14 years 2 months ago
Reachability Analysis for Some Models of Infinite-State Transition Systems
We introduce some new models of infinite-state transition systems. The basic model, called a (reversal-bounded) counter machine (CM), is a nondeterministic finite automaton augment...
Oscar H. Ibarra, Tevfik Bultan, Jianwen Su
CONCUR
2000
Springer
14 years 3 months ago
Formal Models for Communication-Based Design
Concurrency is an essential element of abstract models for embedded systems. Correctness and e ciency of the design depend critically on the way concurrency is formalized and imple...
Alberto L. Sangiovanni-Vincentelli, Marco Sgroi, L...
CONCUR
2000
Springer
14 years 3 months ago
Action Contraction
Abstract. The question we consider in this paper is: “When can a combination of fine-grain execution steps be contracted into an atomic action execution”? Our answer is basica...
Arend Rensink
CONCUR
2000
Springer
14 years 3 months ago
Process Spaces
This paper introduces process spaces, a unified theory of interacting systems. The trait, abstract executions, leads to a simple and general set formalism. For concurrent systems ...
Radu Negulescu
CONCUR
2000
Springer
14 years 3 months ago
Weak Bisimulation for Probabilistic Systems
Abstract. In this paper, we introduce weak bisimulation in the framework of Labeled Concurrent Markov Chains, that is, probabilistic transition systems which exhibit both probabili...
Anna Philippou, Insup Lee, Oleg Sokolsky
CONCUR
2000
Springer
14 years 3 months ago
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata
Abstract. We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in ...
Marta Z. Kwiatkowska, Gethin Norman, Roberto Segal...
CONCUR
2000
Springer
14 years 3 months ago
An Implicitly-Typed Deadlock-Free Process Calculus
Abstract. We extend Kobayashi and Sumii’s type system for the deadlock-free π-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii’s type system helps hig...
Naoki Kobayashi, Shin Saito, Eijiro Sumii
CONCUR
2000
Springer
14 years 3 months ago
LP Deadlock Checking Using Partial Order Dependencies
Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit su...
Victor Khomenko, Maciej Koutny