The Experts below are selected from a list of 651 Experts worldwide ranked by ideXlab platform

Vaandrager F.w. - One of the best experts on this subject based on the ideXlab platform.

  • Source code and data relevant for the paper 'Combining Model Learning and Model Checking to Analyze TCP Implementations'
    DANS EASY, 2017
    Co-Authors: Fiterau-brostean P., Janssen R., Vaandrager F.w.
    Abstract:

    Item does not contain fulltextThe dataset contains source code and data relevant for the paper "Combining Model Learning and Model Checking to Analyze TCP Implementations". Paper url: https://link.springer.com/chapter/10.1007/978-3-319-41540-6_25 PDF url: http://www.sws.cs.ru.nl/publications/papers/fvaan/FJV16/main.pdf Ramon Janssen's Master's thesis url: http://www.ru.nl/publish/pages/769526/z_thesis_ramon_janssen.pdf In this work, we use automata learning with abstraction to infer models of 3 TCP client and server implementations (Windows, Linux, FreeBSD). We then verify properties on these models using the NuSMV model checker. The dataset comprises the software components of our experimental setup apart from the actual implementations, some useful scripts and the learned models and associated experimental logs. In more concrete terms, the dataset contains: - the learner (setup) implementation - Java code for the setup built around LearnLib to perform learning with abstraction over sockets. Abstraction is provided by a mapper, described in a mapper language described in the Master's thesis. - the mapper library - Java code for loading mappers written in the mapper language and executing them in both directions (from abstract to concrete and from concrete to abstract) - the network adapter - crafts packets from strings or messages ("SYN(0,10)") and sends them to a TCP entity, receives packets and turns them back to strings - mappers - the mappers defined for the three operating systems learned - experimental data - Mealy Machine models for 6 TCP client/server implementations (BitVise, OpenSSH, DropBear) accompanied by other experimental data (statistics, input configuration ...) - model checking setup - project comprising bash scripts and Java libraries used to perform model checking on the learned models, model checking is mostly automated What can be re-used: - the learner setup (connect to the learner through the mapper to a different system over sockets), note that there are some limitations of the mapper language - the mapper adapter, again note the limitations which fit the TCP case study but may not fit other case studies - the network adapter, can be adapted to learn other lower layer protocols or can be tweaked to include more information from packets in strings - model checking setup, this cannot really be reused outside of the TCP case study but it may serve as inspiration for one who wants to perform model checking of concretized abstract models (the mappers used to learn the models were also used to concretize them during model checking) or of interactions between two parties - beautifying Java library (if one wants to make complex .dot files more readable) Also, the dataset is suitable for one who wants to try out/expand learning for TCP. Learning and model checking can be done with minimal adaptation (perhaps slight changes in the mapper and adapting the model checking scripts). Paper Abstract: We combine model learning and model checking in a challenging case study involving Linux, Windows and FreeBSD implementations of TCP. We use model learning to infer models of different software components and then apply model checking to fully explore what may happen when these components (e.g. a Linux client and a Windows server) interact. Our analysis reveals several instances in which TCP implementations do not conform to their RFC specifications

  • Learning Register Automata with Fresh Value Generation
    DANS EASY, 2017
    Co-Authors: Aarts Fides, Fiterau-brostean P., Kuppens H.c.w., Vaandrager F.w.
    Abstract:

    Item does not contain fulltextThe dataset contains source code and data relevant for the journal extension of the conference paper "Learning Register Automata with Fresh Value Generation". The journal was due submission at the moment the dataset was made. The journal extension: http://www.sws.cs.ru.nl/publications/papers/fvaan/TomteFresh/main.pdf Conference version: https://link.springer.com/chapter/10.1007/978-3-319-25150-9_11 The dataset also contains some data relevant to an earlier conference paper "'Algorithms for Inferring Register Automata" available at: https://link.springer.com/chapter/10.1007/978-3-662-45234-9_15 In this work, we propose a learning algorithm for register automata and Tomte, a tool implementing this algorithm. Our approach is based on the concept of learning with abstraction, where concrete parameters are abstracted away by a mapper component. Our learning algorithm automatically derives the mapper as well as the abstract Mealy Machine model. From these two we can obtain a concrete register automata model. Peculiar to our approach is that we allow register automata to generate fresh values (arbitrary values). This improves applicability as many real-world system exhibit fresh values. We compare over a series of benchmarks Tomte with RALib, another state-of-the-art tool for register automata. The dataset comprises the Tomte's project files and the SUT Tool's source code. Tomte's project files include experimental data as well as Tomte's source code. The SUT Tool is a tool which Tomte depends on to simulate register automata models or to perform transformations from one type of model to another. In more concrete terms, the dataset contains: - Tomte's implementation - SUT Tool's implementation - experimental data for all works mentioned - various register automata models which can be simulated by the SUT Tool/learned by Tomte What can be re-used: - Tomte (to learn register automata, to perform batch experiements) - SUT Tool (to simulate models or perform transformations) - RALib .jar library (to learn register automata) - the register automata models - stand-alone libraries (like those performing conversion) - parts of the source code easily decoupled from the main flow (graph/tree implementation classes...) Also, the dataset is suitable for one who wants to try out/ extend learning for register automata. Paper Abstract: We present a new algorithm for active learning of register automata. Our algorithm uses counterexample-guided abstraction refinement to automatically construct a component which maps (in a history dependent manner) the large set of actions of an implementation into a small set of actions that can be handled by a Mealy Machine learner. The class of register automata that is handled by our algorithm extends previous definitions since it allows for the generation of fresh output values. This feature is crucial in many real-world systems (e.g. servers that generate identifiers, passwords or sequence numbers). We have implemented our new algorithm in a tool called Tomte. Links: Tomte - usage: http://tomte.cs.ru.nl/Tomte-0-41/Description - source code: https://gitlab.science.ru.nl/harcok/tomte/tree/release-0.41 SUT Tool - usage: http://tomte.cs.ru.nl/Sut-0-4/Description RALib - source code: https://bitbucket.org/learnlib/ralib

  • Learning Register Automata with Fresh Value Generation
    DANS EASY, 2017
    Co-Authors: Aarts Fides, Fiterau-brostean P., Kuppens H.c.w., Vaandrager F.w.
    Abstract:

    The dataset contains source code and data relevant for the journal extension of the conference paper "Learning Register Automata with Fresh Value Generation". The journal was due submission at the moment the dataset was made. The journal extension: http://www.sws.cs.ru.nl/publications/papers/fvaan/TomteFresh/main.pdf Conference version: https://link.springer.com/chapter/10.1007/978-3-319-25150-9_11 The dataset also contains some data relevant to an earlier conference paper "'Algorithms for Inferring Register Automata" available at: https://link.springer.com/chapter/10.1007/978-3-662-45234-9_15 In this work, we propose a learning algorithm for register automata and Tomte, a tool implementing this algorithm. Our approach is based on the concept of learning with abstraction, where concrete parameters are abstracted away by a mapper component. Our learning algorithm automatically derives the mapper as well as the abstract Mealy Machine model. From these two we can obtain a concrete register automata model. Peculiar to our approach is that we allow register automata to generate fresh values (arbitrary values). This improves applicability as many real-world system exhibit fresh values. We compare over a series of benchmarks Tomte with RALib, another state-of-the-art tool for register automata. The dataset comprises the Tomte's project files and the SUT Tool's source code. Tomte's project files include experimental data as well as Tomte's source code. The SUT Tool is a tool which Tomte depends on to simulate register automata models or to perform transformations from one type of model to another. In more concrete terms, the dataset contains: - Tomte's implementation - SUT Tool's implementation - experimental data for all works mentioned - various register automata models which can be simulated by the SUT Tool/learned by Tomte What can be re-used: - Tomte (to learn register automata, to perform batch experiements) - SUT Tool (to simulate models or perform transformations) - RALib .jar library (to learn register automata) - the register automata models - stand-alone libraries (like those performing conversion) - parts of the source code easily decoupled from the main flow (graph/tree implementation classes...) Also, the dataset is suitable for one who wants to try out/ extend learning for register automata. Paper Abstract: We present a new algorithm for active learning of register automata. Our algorithm uses counterexample-guided abstraction refinement to automatically construct a component which maps (in a history dependent manner) the large set of actions of an implementation into a small set of actions that can be handled by a Mealy Machine learner. The class of register automata that is handled by our algorithm extends previous definitions since it allows for the generation of fresh output values. This feature is crucial in many real-world systems (e.g. servers that generate identifiers, passwords or sequence numbers). We have implemented our new algorithm in a tool called Tomte. Links: Tomte - usage: http://tomte.cs.ru.nl/Tomte-0-41/Description - source code: https://gitlab.science.ru.nl/harcok/tomte/tree/release-0.41 SUT Tool - usage: http://tomte.cs.ru.nl/Sut-0-4/Description RALib - source code: https://bitbucket.org/learnlib/ralib

Michael Luttenberger - One of the best experts on this subject based on the ideXlab platform.

  • Practical synthesis of reactive systems from LTL specifications via parity games
    Acta Informatica, 2020
    Co-Authors: Michael Luttenberger, Philipp J Meyer, Salomon Sickert
    Abstract:

    The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions ( Syntcomp2018 / 2019 ). The presented approach is (1) structured , meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy Machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.

  • strix explicit reactive synthesis strikes back
    Computer Aided Verification, 2018
    Co-Authors: Philipp J Meyer, Salomon Sickert, Michael Luttenberger
    Abstract:

    Strix is a new tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games. In brief, Strix (1) decomposes the given formula into simpler formulas, (2) translates these on-the-fly into DPAs based on the queries of the parity game solver, (3) composes the DPAs into a parity game, and at the same time already solves the intermediate games using strategy iteration, and (4) finally translates the winning strategy, if it exists, into a Mealy Machine or an AIGER circuit with optional minimization using external tools. We experimentally demonstrate the applicability of our approach by a comparison with Party, BoSy, and ltlsynt using the syntcomp2017 benchmarks. In these experiments, our prototype can compete with BoSy and ltlsynt with only Party performing slightly better. In particular, our prototype successfully synthesizes the full and unmodified LTL specification of the AMBA protocol for \(n=2\) masters.

Jaijeet Roychowdhury - One of the best experts on this subject based on the ideXlab platform.

  • fsm model abstraction for analog mixed signal circuits by learning from i o trajectories
    Asia and South Pacific Design Automation Conference, 2011
    Co-Authors: Jaijeet Roychowdhury
    Abstract:

    Abstraction of circuits is desirable for faster simulation and high-level system verification. In this paper, we present an algorithm that derives a Mealy Machine from differential equations of a circuit by learning input-output trajectories. The key idea is adapted from Angluin's DFA (deterministic finite automata) learning algorithm [1] that learns a DFA from another DFA. Several key components of Angluin's algorithm are modified so that it fits in our problem setting, and the modified algorithm also provides a reasonable partitioning of the continuous state space as a by-product. We validate our algorithm on a latch circuit and an integrator circuit, and demonstrate that the resulting FSMs inherit important behaviors of original circuits.

  • FSM model abstraction for analog/mixed-signal circuits by learning from I/O trajectories
    2011
    Co-Authors: Jaijeet Roychowdhury
    Abstract:

    Abstract—Abstraction of circuits is desirable for faster simulation and high-level system verification. In this paper, we present an algorithm that derives a Mealy Machine from differential equations of a circuit by learning input-output trajectories. The key idea is adapted from Angluin’s DFA (deterministic finite automata) learning algorithm [1] that learns a DFA from another DFA. Several key components of Angluin’s algorithm are modified so that it fits in our problem setting, and the modified algorithm also provides a reasonable partitioning of the continuous state space as a by-product. We validate our algorithm on a latch circuit and an integrator circuit, and demonstrate that the resulting FSMs inherit important behaviors of original circuits. I

Lee C. Giles - One of the best experts on this subject based on the ideXlab platform.

  • Learning Communication for Multi-agent Systems
    Springer, 2002
    Co-Authors: Lee C. Giles, Kam-chuen Jim
    Abstract:

    We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to learn multi-agent languages for the predator agents in a version of the predator-prey problem. The resulting evolved behavior of the communicating multi-agent system is equivalent to that of a Mealy Machine whose states are determined by the evolved language. We also constructed non-learning predators whose capture behavior was designed to take advantage of prey behavior known a priori. Simulations show that introducing noise to the decision process of the hard-coded predators allow them to significantly ourperform all previously published work on similar preys. Furthermore, the evolved communicating predators were able to perform significantly better than the hard-coded predators, which indicates that the system was able to learn superior communicating strategies not readily available to the human designer

  • Agents for the Predator-Prey Pursuit Problem
    2001
    Co-Authors: Kam-chuen Jim, Lee C. Giles
    Abstract:

    We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to evolve multi-agent languages for the predator agents in a version of the predator-prey pursuit problem. We show that the resulting behavior of the communicating multi-agent system is equivalent to that of a Mealy finite state Machine whose states are determined by the agents ’ usage of the evolved language. Simulations show that the evolution of a communication language improves the performance of the predators. Increasing the language size (and thus increasing the number of possible states in the Mealy Machine) improves the performance even further. Furthermore, the evolved communicating predators perform significantly better than all previous work on similar preys. We introduce a method for incrementally increasing the language size which results in an effective coarse-to-fin

  • Talking helps: Evolving communicating agents for the predator-prey pursuit problem
    2000
    Co-Authors: Kam-chuen Jim, Lee C. Giles
    Abstract:

    Abstract We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to evolve multi-agent languages for the predator agents in a version of the predator-prey pursuit problem. We show that the resulting behavior of the communicating multi-agent system is equivalent to that of a Mealy �nite state Machine whose states are determined by the agents ’ usage of the evolved language. Simulations show that the evolution of a communication language improves the performance of the predators. Increasing the language size (and thus increasing the number of possible states in the Mealy Machine) improves the performance even further. Furthermore, the evolved communicating predators perform signi�cantly better than all previous work on similar prey. We introduce a method fo

  • Talking Helps: Evolving Communicating Agents for the Predator-Prey Pursuit Problem
    2000
    Co-Authors: Kam-chuen Jim, Lee C. Giles
    Abstract:

    We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to evolve multi-agent languages for the predator agents in a version of the predator-prey pursuit problem. We show that the resulting behavior of the communicating multi-agent system is equivalent to that of a Mealy finite state Machine whose states are determined by the agents' usage of the evolved language. Simulations show that the evolution of a communication language improves the performance of the predators. Increasing the language size (and thus increasing the number of possible states in the Mealy Machine) improves the performance even further. Furthermore, the evolved communicating predators perform significantly better than all previous work on similar preys. We introduce a method for incrementally increasing the language size which results in an effective coarse-to-fine search that significantly reduces the evolution time required to find a solution. We present some observations on the effects of language size, experimental setup, and prey difficulty on the evolved Mealy Machines. In particular, we observe that the start state is often revisited, and incrementally increasing the language size results in smaller Mealy Machines. Finally, a simple rule is derived that provides a pessimistic estimate on the minimum language size that should be used for any multi-agent problem.

Kam-chuen Jim - One of the best experts on this subject based on the ideXlab platform.

  • Learning Communication for Multi-agent Systems
    Springer, 2002
    Co-Authors: Lee C. Giles, Kam-chuen Jim
    Abstract:

    We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to learn multi-agent languages for the predator agents in a version of the predator-prey problem. The resulting evolved behavior of the communicating multi-agent system is equivalent to that of a Mealy Machine whose states are determined by the evolved language. We also constructed non-learning predators whose capture behavior was designed to take advantage of prey behavior known a priori. Simulations show that introducing noise to the decision process of the hard-coded predators allow them to significantly ourperform all previously published work on similar preys. Furthermore, the evolved communicating predators were able to perform significantly better than the hard-coded predators, which indicates that the system was able to learn superior communicating strategies not readily available to the human designer

  • Agents for the Predator-Prey Pursuit Problem
    2001
    Co-Authors: Kam-chuen Jim, Lee C. Giles
    Abstract:

    We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to evolve multi-agent languages for the predator agents in a version of the predator-prey pursuit problem. We show that the resulting behavior of the communicating multi-agent system is equivalent to that of a Mealy finite state Machine whose states are determined by the agents ’ usage of the evolved language. Simulations show that the evolution of a communication language improves the performance of the predators. Increasing the language size (and thus increasing the number of possible states in the Mealy Machine) improves the performance even further. Furthermore, the evolved communicating predators perform significantly better than all previous work on similar preys. We introduce a method for incrementally increasing the language size which results in an effective coarse-to-fin

  • Talking helps: Evolving communicating agents for the predator-prey pursuit problem
    2000
    Co-Authors: Kam-chuen Jim, Lee C. Giles
    Abstract:

    Abstract We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to evolve multi-agent languages for the predator agents in a version of the predator-prey pursuit problem. We show that the resulting behavior of the communicating multi-agent system is equivalent to that of a Mealy �nite state Machine whose states are determined by the agents ’ usage of the evolved language. Simulations show that the evolution of a communication language improves the performance of the predators. Increasing the language size (and thus increasing the number of possible states in the Mealy Machine) improves the performance even further. Furthermore, the evolved communicating predators perform signi�cantly better than all previous work on similar prey. We introduce a method fo

  • Talking Helps: Evolving Communicating Agents for the Predator-Prey Pursuit Problem
    2000
    Co-Authors: Kam-chuen Jim, Lee C. Giles
    Abstract:

    We analyze a general model of multi-agent communication in which all agents communicate simultaneously to a message board. A genetic algorithm is used to evolve multi-agent languages for the predator agents in a version of the predator-prey pursuit problem. We show that the resulting behavior of the communicating multi-agent system is equivalent to that of a Mealy finite state Machine whose states are determined by the agents' usage of the evolved language. Simulations show that the evolution of a communication language improves the performance of the predators. Increasing the language size (and thus increasing the number of possible states in the Mealy Machine) improves the performance even further. Furthermore, the evolved communicating predators perform significantly better than all previous work on similar preys. We introduce a method for incrementally increasing the language size which results in an effective coarse-to-fine search that significantly reduces the evolution time required to find a solution. We present some observations on the effects of language size, experimental setup, and prey difficulty on the evolved Mealy Machines. In particular, we observe that the start state is often revisited, and incrementally increasing the language size results in smaller Mealy Machines. Finally, a simple rule is derived that provides a pessimistic estimate on the minimum language size that should be used for any multi-agent problem.