Sciweavers

IFM
2010
Springer
159views Formal Methods» more  IFM 2010»
13 years 10 months ago
A Logical Framework to Deal with Variability
We present a logical framework that is able to deal with variability in product family descriptions. The temporal logic MHML is based on the classical Hennessy–Milner logic with ...
Patrizia Asirelli, Maurice H. ter Beek, Alessandro...
JSA
2008
131views more  JSA 2008»
13 years 11 months ago
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describ...
Amjad Gawanmeh, Sofiène Tahar, Kirsten Wint...
ENTCS
2002
95views more  ENTCS 2002»
13 years 11 months ago
Deriving Bisimulation Congruences: A 2-categorical Approach
We introduce G-relative-pushouts (GRPO) which are a 2-categorical generalisation of relative-pushouts (RPO). They are suitable for deriving labelled transition systems (LTS) for p...
Vladimiro Sassone, Pawel Sobocinski
LOGCOM
2007
97views more  LOGCOM 2007»
13 years 11 months ago
A General Framework for Expressing Preferences in Causal Reasoning and Planning
We consider the problem of incorporating arbitrary preferences in planning systems. A preference may be seen as a goal or constraint that is desirable, but not necessary, to satis...
James P. Delgrande, Torsten Schaub, Hans Tompits
ENTCS
2007
111views more  ENTCS 2007»
13 years 11 months ago
Multi Labelled Transition Systems: A Semantic Framework for Nominal Calculi
Action Labelled transition systems (LTS) have proved to be a fundamental model for describing and proving properties of concurrent systems. In this paper,Multiple Labelled Transit...
Rocco De Nicola, Michele Loreti
ENTCS
2007
96views more  ENTCS 2007»
13 years 11 months ago
Semantics of Biological Regulatory Networks
The aim of the paper is to revisit the model of Biological Regulatory Networks (BRN) which was proposed by René Thomas to model the interactions between a set of genes. We give a...
Gilles Bernot, Franck Cassez, Jean-Paul Comet, Fra...
ENTCS
2007
121views more  ENTCS 2007»
13 years 11 months ago
An Account of Implementing Applicative Term Rewriting
Generation of labelled transition systems from system specifications is highly dependent on efficient rewriting (or related techniques). We give an account of the implementation ...
Muck van Weerdenburg
LOGCOM
2008
60views more  LOGCOM 2008»
13 years 11 months ago
Monotonic and Downward Closed Games
In an earlier work [Abdulla et al. (2000, Information and Computation, 160, 109
Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Ors...
JALC
2006
61views more  JALC 2006»
13 years 11 months ago
Random Polynomial-Time Attacks and Dolev-Yao Models
In this paper we present an extension of Dolev-Yao models for security protocols with a notion of random polynomial-time (Las Vegas) computability. First we notice that Dolev-Yao ...
Mathieu Baudet
JLP
2008
98views more  JLP 2008»
13 years 11 months ago
Comparing disjunctive modal transition systems with an one-selecting variant
models, used for specification, analysis and verification, usually describe sets of implementations by means of a refinement relation. In the branching time setting, implementatio...
Harald Fecher, Heiko Schmidt