Sciweavers

FOSSACS
2007
Springer
15 years 10 months ago
Model-Checking One-Clock Priced Timed Automata
Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Ma...
156
Voted
FOSSACS
2007
Springer
15 years 10 months ago
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested “stack of stacks” structure. These systems may be us...
Matthew Hague, C.-H. Luke Ong
FOSSACS
2007
Springer
15 years 10 months ago
Iterator Types
Abstract. System L is a linear λ-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of G¨odel’s Sy...
Sandra Alves, Maribel Fernández, Már...
FOSSACS
2007
Springer
15 years 10 months ago
Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
We give logical characterizations of bisimulation relations for the probabilistic automata of Segala in terms of three Hennessy-Milner style logics. The three logics characterize s...
Augusto Parma, Roberto Segala
FOSSACS
2007
Springer
15 years 10 months ago
Semantic Barbs and Biorthogonality
We use the framework of biorthogonality to introduce a novel semantic definition of the concept of barb (basic observable) for process calculi. We develop a uniform basic theory o...
Julian Rathke, Vladimiro Sassone, Pawel Sobocinski
FOSSACS
2007
Springer
15 years 10 months ago
Generalized Parity Games
Krishnendu Chatterjee, Thomas A. Henzinger, Nir Pi...
130
Voted
FOSSACS
2007
Springer
15 years 10 months ago
Tree Automata with Memory, Visibility and Structural Constraints
Tree automata with one memory have been introduced in
Hubert Comon-Lundh, Florent Jacquemard, Nicolas Pe...
FOSSACS
2007
Springer
15 years 10 months ago
Logical Reasoning for Higher-Order Functions with Local State
Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically an...
Nobuko Yoshida, Kohei Honda, Martin Berger
FOSSACS
2007
Springer
15 years 10 months ago
On the Expressiveness and Complexity of ATL
ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions...
François Laroussinie, Nicolas Markey, Ghass...