Sciweavers

FOSSACS
2009
Springer
13 years 8 months ago
On Omega-Languages Defined by Mean-Payoff Conditions
In quantitative verification, system states/transitions have associated costs, and these are used to associate mean-payoff costs with infinite behaviors. In this paper, we propose ...
Rajeev Alur, Aldric Degorre, Oded Maler, Gera Weis...
FOSSACS
2009
Springer
13 years 8 months ago
The Calculus of Handshake Configurations
Handshake protocols are asynchronous protocols that enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. W...
Luca Fossati, Daniele Varacca
FOSSACS
2009
Springer
13 years 8 months ago
Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains
We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes ...
Morten Kühnrich, Stefan Schwoon, Jirí ...
FOSSACS
2009
Springer
13 years 11 months ago
On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
Higher-order recursion schemes are systems of rewrite rules on typed non-terminal symbols, which can be used to define infinite trees. The Global Modal Mu-Calculus Model Checking...
Christopher Broadbent, C.-H. Luke Ong
FOSSACS
2009
Springer
13 years 11 months ago
Reactive Systems, Barbed Semantics, and the Mobile Ambients
Reactive systems, proposed by Leifer and Milner, represent a meta-framework aimed at deriving behavioral congruences for those specification formalisms whose operational semantics...
Filippo Bonchi, Fabio Gadducci, Giacoma Valentina ...
FOSSACS
2009
Springer
13 years 11 months ago
Bisimulation for Demonic Schedulers
Bisimulation between processes has been proven a successful method for formalizing security properties. We argue that in certain cases, a scheduler that has full information on the...
Konstantinos Chatzikokolakis, Gethin Norman, David...
FOSSACS
2009
Springer
13 years 11 months ago
Separating Graph Logic from MSO
Abstract. Graph logic (GL) is a spatial logic for querying graphs introduced by Cardelli et al. It has been observed that in terms of expressive power, this logic is a fragment of ...
Timos Antonopoulos, Anuj Dawar
FOSSACS
2009
Springer
13 years 11 months ago
A Kleene Theorem for Polynomial Coalgebras
Marcello M. Bonsangue, Jan J. M. M. Rutten, Alexan...
FOSSACS
2009
Springer
13 years 11 months ago
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
Abstract. We present a realizability model for a call-by-value, higherorder programming language with parametric polymorphism, general first-class references, and recursive types....
Lars Birkedal, Kristian Støvring, Jacob Tha...