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...
Handshake protocols are asynchronous protocols that enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. W...
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 ...
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...
Reactive systems, proposed by Leifer and Milner, represent a meta-framework aimed at deriving behavioral congruences for those specification formalisms whose operational semantics...
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...
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 ...
Abstract. We present a realizability model for a call-by-value, higherorder programming language with parametric polymorphism, general first-class references, and recursive types....