Arrow Research search

Author name cluster

Axel Legay

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

19 papers
2 author rows

Possible papers

19

EAAI Journal 2024 Journal Article

Feature selection for packer classification based on association rule mining

  • Rosana Veroneze
  • Charles-Henry Bertrand Van Ouytsel
  • Khanh Huu The Dam
  • Axel Legay

Malware often uses packing, an obfuscation strategy, to bypass antivirus. Identifying and understanding packers is therefore essential for analyzing suspicious binary files. Proposed machine learning methods for packer classification use a wide range of features, but many of them are redundant or irrelevant. It leads to waste of computational resources, so minimizing such features without reducing the effectiveness of packer identification is essential to analyze the ever-growing number of malware. This paper presents a novel embedded feature selection method for packer classification named Feature Selection based on Associative Classification (FSbAC). FSbAC exploits established concepts of association rule mining, particularly associative classification. As a result, FSbAC can define important sets of features per each packer individually, not just for the entire dataset. This makes it possible to directly learn the characteristics of each packer, improving the knowledge of analysts against packing. It also allows the costs associated with feature extraction to be taken into account during the selection process, ensuring the efficiency of the selected feature set. Seven different classification algorithms were used to assess the performance of FSbAC against eight FS methods. The evaluation encompassed different scenarios of packer classification, employing both a synthetic dataset and real-world datasets. The performance of the FS methods was evaluated with and without the inclusion of byte features vulnerable to bypass by hackers. Our results indicate that FSbAC is efficient for packer classification and leads to a substantial decrease in the number of features and in the computational resources required, without compromising predictive performance.

TCS Journal 2020 Journal Article

Computing branching distances with quantitative games

  • Uli Fahrenberg
  • Axel Legay
  • Karin Quaas

We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.

TCS Journal 2020 Journal Article

Expressiveness of concurrent intensionality

  • Ioana Cristescu
  • Thomas Given-Wilson
  • Axel Legay

The expressiveness of communication primitives has been explored in a common framework based on the π-calculus by considering four features: synchronism (asynchronous vs synchronous), arity (monadic vs polyadic data), communication medium (shared dataspaces vs channel-based), and pattern-matching (binding to a name vs testing name equality). Here pattern-matching is generalised to account for terms with internal structure such as in recent calculi like Spi calculi, Concurrent Pattern Calculus and Psi calculi. This paper explores intensionality, a feature that extends pattern-matching to allow communication primitives to interact by also matching on the structure of terms. By means of possibility/impossibility of encodings, this paper shows that intensionality alone can encode synchronism, arity, communication-medium, and pattern-matching, yet no combination of these without intensionality can encode any intensional language. Further, some languages may also be non-linear, where two inputs must be equal to allow interaction. This paper also explores all the relations between linear and non-linear variations of the above languages.

TCS Journal 2020 Journal Article

Generalized abstraction-refinement for game-based CTL lifted model checking

  • Aleksandar S. Dimovski
  • Axel Legay
  • Andrzej Wasowski

System families (Software Product Lines) are becoming omnipresent in application areas ranging from embedded system domains to system-level software and communication protocols. Software Product Line methods and architectures allow effective building many custom variants of a software system in these domains. In many of the applications, their rigorous verification and quality assurance are of paramount importance. Lifted model checking for system families is capable of verifying all their variants simultaneously in a single run by exploiting the similarities between the variants. The computational cost of lifted model checking still greatly depends on the number of variants (the size of configuration space), which is often huge. Variability abstractions have successfully addressed this configuration space explosion problem, giving rise to smaller abstract variability models with fewer abstract configurations. Abstract variability models are given as modal transition systems, which contain may (over-approximating) and must (under-approximating) transitions. Thus, they preserve both universal and existential CTL properties. In this work, we bring two main contributions. First, we define a novel game-based approach for variability-specific abstraction and refinement for lifted model checking of the full CTL, interpreted over 3-valued semantics. We propose a direct algorithm for solving a 3-valued (abstract) lifted model checking game. In case the result of model checking an abstract variability model is indefinite, we suggest a new notion of refinement, which eliminates indefinite results. This provides an iterative incremental variability-specific abstraction and refinement framework, where refinement is applied only where indefinite results exist and definite results from previous iterations are reused. Second, we propose a new generalized definition of abstract variability models, given as so-called generalized modal transition systems, by introducing the notion of (must) hyper-transitions. This results in more precise abstract models in which more CTL formulae can be proved or disproved. We integrate the newly defined generalized abstract variability models in the existing abstraction-refinement framework for game-based lifted model checking of CTL. Finally, we evaluate the practicality of this approach on several system families.

I&C Journal 2020 Journal Article

Logical vs. behavioural specifications

  • Nikola Beneš
  • Uli Fahrenberg
  • Jan Křetínský
  • Axel Legay
  • Louis-Marie Traonouez

There are two fundamentally different approaches for specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of ν-calculus and the behavioural formalism of disjunctive modal transition systems. The translations preserve structural properties of the input specification and allow us to perform logical operations on the behavioural specifications as well as behavioural compositions on logical formulae. The unification of both approaches provides additional methods for component-based stepwise design.

FormaliSE Conference 2019 Conference Paper

Towards sampling and simulation-based analysis of featured weighted automata

  • Maxime Cordy
  • Axel Legay
  • Sami Lazreg
  • Philippe Collet

We consider the problem of model checking Variability-Intensive Systems (VIS) against non-functional requirements. These requirements are typically expressed as an optimization problem over quality attributes of interest, whose value is determined by the executions of the system. Identifying the optimal variant can be hard due to the state-explosion problem inherent to model checking the exponentially growing number of variants in large VIS. In this paper, we lay the foundations for the application of smart sampling and statistical model checking to solve this problem faster. We design a simple method that samples variants and executions in a uniform manner from a featured weighted automaton and that assesses which of the sampled variants/executions are optimal. We implemented our approach on top of ProVeLines, a tool suite for model-checking VIS and carried out a preliminary evaluation on an industrial embedded system design case study. Our results show that sampling-based approaches indeed holds the potential to improve scalability but should be supported by better heuristics to be competitive.

FormaliSE Conference 2017 Conference Paper

Featured Weighted Automata

  • Uli Fahrenberg
  • Axel Legay

A featured transition system is a transition system in which the transitions are annotated with feature expressions: Boolean expressions on a finite number of given features. Depending on its feature expression, each individual transition can be enabled when some features are present, and disabled for other sets of features. The behavior of a featured transition system hence depends on a given set of features. There are algorithms for featured transition systems which can check their properties for all sets of features at once, for example for LTL or CTL properties. Here we introduce a model of featured weighted automata which combines featured transition systems and (semiring-) weighted automata. We show that methods and techniques from weighted automata extend to featured weighted automata and devise algorithms to compute quantitative properties of featured weighted automata for all sets of features at once. We show applications to minimum reachability and to energy properties.

TCS Journal 2016 Journal Article

Command-based importance sampling for statistical model checking

  • Cyrille Jegourel
  • Axel Legay
  • Sean Sedwards

Statistical model checking avoids the exponential growth of states of numerical model checking, but rare properties are costly to verify. Importance sampling can reduce the cost if good importance sampling distributions can be found efficiently. Our approach uses a tractable cross-entropy minimisation algorithm to find an optimal parametrised importance sampling distribution. In contrast to previous work, our algorithm uses a naturally defined low dimensional vector to specify the distribution, thus avoiding an explicit representation of a transition matrix. Our parametrisation leads to a unique optimum and is shown to produce many orders of magnitude improvement in efficiency on various models. In this work we link the existence of optimal importance sampling distributions to logical properties and show how our parametrisation affects this link. We also motivate and present simple algorithms to create the initial distribution necessary for cross-entropy minimisation. Finally, we discuss the open challenge of defining error bounds with importance sampling and describe how our optimal parametrised distributions may be used to infer qualitative confidence.

FormaliSE Conference 2015 Conference Paper

Measuring Behaviour Interactions between Product-Line Features

  • Joanne M. Atlee
  • Uli Fahrenberg
  • Axel Legay

We suggest a method for measuring the degree to which features interact in feature-oriented software development. To this end, we extend the notion of simulation between transition systems to a similarity measure and lift it to compute a behaviour interaction score in featured transition systems. We then develop an algorithm which can compute the degree of feature interactions in a featured transition system in an efficient manner.

TCS Journal 2015 Journal Article

Quantifying information leakage of randomized protocols

  • Fabrizio Biondi
  • Axel Legay
  • Pasquale Malacaria
  • Andrzej Wąsowski

The quantification of information leakage provides a quantitative evaluation of the security of a system. We propose the usage of Markovian processes to model deterministic and probabilistic systems. By using a methodology generalizing the lattice of information approach we model refined attackers capable to observe the internal behavior of the system, and quantify the information leakage of such systems. We also use our method to obtain an algorithm for the computation of channel capacity from our Markovian models. Finally, we show how to use the method to analyze timed and non-timed attacks on the Onion Routing protocol.

TCS Journal 2014 Journal Article

Robust synthesis for real-time systems

  • Kim G. Larsen
  • Axel Legay
  • Louis-Marie Traonouez
  • Andrzej Wąsowski

Specification theories for real-time systems allow reasoning about interfaces and their implementation models, using a set of operators that includes satisfaction, refinement, logical and parallel composition. To make such theories applicable throughout the entire design process from an abstract specification to an implementation, we need to reason about the possibility to effectively implement the theoretical specifications on physical systems, despite their limited precision. In the literature, this implementation problem has been linked to the robustness problem that analyzes the consequences of introducing small perturbations into formal models. We address this problem of robust implementations in timed specification theories. We first consider a fixed perturbation and study the robustness of timed specifications with respect to the operators of the theory. To this end we synthesize robust strategies in timed games. Finally, we consider the parametric robustness problem and propose a counter-example refinement heuristic for computing safe perturbation values.

TCS Journal 2014 Journal Article

The quantitative linear-time–branching-time spectrum

  • Uli Fahrenberg
  • Axel Legay

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.

FormaliSE Conference 2013 Conference Paper

A framework for the rigorous design of highly adaptive timed systems

  • Maxime Cordy
  • Axel Legay
  • Pierre-Yves Schobbens
  • Louis-Marie Traonouez

Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in response to unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.

I&C Journal 2013 Journal Article

Abstract Probabilistic Automata

  • Benoît Delahaye
  • Joost-Pieter Katoen
  • Kim G. Larsen
  • Axel Legay
  • Mikkel L. Pedersen
  • Falak Sher
  • Andrzej Wąsowski

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In APAs uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behavior is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.

I&C Journal 2013 Journal Article

Pushdown module checking with imperfect information

  • Benjamin Aminof
  • Axel Legay
  • Aniello Murano
  • Olivier Serre
  • Moshe Y. Vardi

The model checking problem for finite-state open systems (module checking) has been extensively studied in the literature, both in the context of environments with perfect and imperfect information about the system. Recently, the perfect information case has been extended to infinite-state systems (pushdown module checking). In this paper, we extend pushdown module checking to the imperfect information setting; i. e. , to the case where the environment has only a partial view of the systemʼs control states and pushdown store content. We study the complexity of this problem with respect to the branching-time temporal logics CTL, CTL ⁎ and the propositional μ-calculus. We show that pushdown module checking, which is by itself harder than pushdown model checking, becomes undecidable when the environment has imperfect information. We also show that undecidability relies on hiding information about the pushdown store. Indeed, we prove that with imperfect information about the control states, but a visible pushdown store, the problem is decidable and its complexity is 2Exptime-complete for CTL and the propositional μ-calculus, and 3Exptime-complete for CTL ⁎.

LPAR Conference 2012 Conference Paper

Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic

  • Peter E. Bulychev
  • Alexandre David
  • Kim G. Larsen
  • Axel Legay
  • Guangyuan Li
  • Danny Bøgsted Poulsen
  • Amélie Stainer

Abstract We present a novel approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric temporal logic (WMTL ≤ ). Based on a stochastic semantics of WTAs, we apply statistical model checking (SMC) to estimate and test probabilities of satisfaction with desired levels of confidence. Our approach consists in generation of deterministic monitors for formulas in WMTL ≤, allowing for efficient SMC by run-time evaluation of a given formula. By necessity, the deterministic observers are in general approximate (over- or under-approximations), but are most often exact and experimentally tight. The technique is implemented in the new tool Casaal. that we seamlessly connect to Uppaal-smc. in a tool chain. We demonstrate the applicability of our technique and the efficiency of our implementation through a number of case-studies.

TCS Journal 2011 Journal Article

Constraint Markov Chains

  • Benoît Caillaud
  • Benoît Delahaye
  • Kim G. Larsen
  • Axel Legay
  • Mikkel L. Pedersen
  • Andrzej Wąsowski

Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constitute a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable.

TCS Journal 2011 Journal Article

Hardness of preorder checking for basic formalisms

  • Laura Bozzelli
  • Axel Legay
  • Sophie Pinchinat

We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a standard timed automaton. In both cases, we show that simulation checking is Exptime-hard, and for the case of a non-flat implementation, the result holds even if there is no synchronization between the parallel components and their alphabets of actions are pairwise disjoint. Moreover, we show that the considered problems become Pspace-complete when the specification is assumed to be deterministic. Additionally, we establish that comparing a synchronous non-flat system with no hiding and a flat system is Pspace-hard for any relation between trace containment and bisimulation equivalence, even if the flat system is assumed to be fixed.

MFCS Conference 2011 Conference Paper

Quantitative Refinement for Weighted Modal Transition Systems

  • Sebastian S. Bauer
  • Uli Fahrenberg
  • Line Juhl
  • Kim G. Larsen
  • Axel Legay
  • Claus R. Thrane

Abstract Specification theories as a tool in the development process of component-based software systems have recently attracted a considerable attention. Current specification theories are however qualitative in nature and hence fragile and unsuited for modern software systems. We propose the first specification theory which allows to capture quantitative aspects during the refinement and implementation process.

v2026.09.13