Nicolas Markey

Résumé

In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

@inproceedings{rv2024-HJMR,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas and Roussanaly, Victor},
  title =               {Distributed Monitoring of Timed Properties},
  editor =              {{\'A}brah{\'a}m, Erikz and Abbas, Houssam},
  booktitle =           {{P}roceedings of the 24th {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'24)},
  acronym =             {{RV}'24},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {15191},
  pages =               {243-261},
  year =                {2024},
  month =               oct,
  doi =                 {10.1007/978-3-031-74234-7_16},
  abstract =            {In formal verification, runtime monitoring consists
                         of observing the execution of a system in order to
                         decide as quickly as possible whether or not it
                         satisfies a given property. We consider monitoring
                         in a distributed setting, for properties given as
                         reachability timed automata. In~such a setting,
                         the~system is made of several components, each
                         equipped with its own local clock and monitor.
                         The~monitors observe events occurring on their
                         associated component, and receive timestamped events
                         from other monitors through FIFO channels. Since
                         clocks are local, they cannot be perfectly
                         synchronized, resulting in imprecise timestamps.
                         Consequently, they must be seen as intervals,
                         leading monitors to consider possible reorderings of
                         events. In this context, each monitor aims to
                         provide, as early as possible, a verdict on the
                         property it is monitoring, based on its potentially
                         incomplete and imprecise knowledge of the current
                         execution. In~this~paper, we~propose an on-line
                         monitoring algorithm for timed properties, robust to
                         time imprecision and partial information from
                         distant components. We~first identify the date at
                         which a monitor can safely compute a verdict based
                         on received events. We~then propose a monitoring
                         algorithm that updates this date when new
                         information arrives, maintains the current set of
                         states in which the property can reside, and updates
                         its verdict accordingly.},
}

Résumé

We introduce a new class of automata (which we coin EU-automata) running on infininte trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata.

We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logic QCTL (which extends CTL with quantification over atomic propositions) and for MSO. On the one hand, we obtain decision procedures with optimal complexity for QCTL satisfiability and model checking; on the other hand, we obtain an algorithm for translating any QCTL formula with k quantifier alternations to formulas with at most one quantifier alternation, at the expense of a (k+1)-exponential blow-up in the size of the formulas. Using the same techniques, we prove that any MSO formula can be translated into a formula with at most four quantifier alternations (and only two second-order-quantifier alternations), again with a (k+1)-exponential blow-up in the size of the formula.

@techreport{arxiv2410.18799-LM,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas},
  title =               {Arbitrary-arity Tree Automata and QCTL},
  number =              {2410.18799},
  year =                {2024},
  month =               oct,
  doi =                 {10.48550/arXiv.2410.18799},
  institution =         {arXiv},
  abstract =            {We~introduce a new class of automata (which we coin
                         \emph{EU-automata}) running on infininte trees of
                         arbitrary (finite) arity. We~develop and study
                         several algorithms to perform classical operations
                         (union, intersection, complement, projection,
                         alternation removal) for those automata, and
                         precisely characterise their complexities. We~also
                         develop algorithms for solving membership and
                         emptiness for the languages of trees accepted by
                         EU-automata. \par We~then use EU-automata to obtain
                         several algorithmic and expressiveness results for
                         the temporal logic \textsf{QCTL} (which extends
                         \textsf{CTL} with quantification over atomic
                         propositions) and for \textsf{MSO}. On the one hand,
                         we obtain decision procedures with optimal
                         complexity for \textsf{QCTL} satisfiability and
                         model checking; on the other hand, we obtain an
                         algorithm for translating any \textsf{QCTL} formula
                         with \(k\) quantifier alternations to formulas with
                         at most one quantifier alternation, at~the~expense
                         of a \((k+1)\)-exponential blow-up in the size of
                         the formulas. Using the same techniques, we~prove
                         that any \textsf{MSO} formula can be translated into
                         a formula with at most four quantifier alternations
                         (and only two second-order-quantifier alternations),
                         again with a \((k+1)\)-exponential blow-up in the
                         size of the formula.},
}

@inproceedings{fossacs2024-Pra,
  author =              {Prakash, Aditya},
  title =               {Checking History-Determinism is {NP}-hard for Parity
                         Automata},
  editor =              {Kobayashi, Naoki and Worrell, James},
  booktitle =           {{P}roceedings of the 27th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'24)},
  acronym =             {{FoSSaCS}'24},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {14574},
  pages =               {212-233},
  year =                {2024},
  month =               apr,
  doi =                 {10.1007/978-3-031-57228-9_11},
}

Résumé

We consider the automatic online synthesis of black-box test cases from functional requirements specified as automata for reactive implementations. The goal of the tester is to reach some given state, so as to satisfy a coverage criterion, while monitoring the violation of the requirements. We develop an approach based on Monte Carlo Tree Search, which is a classical technique in reinforcement learning for efficiently selecting promising inputs. Seeing the automata requirements as a game between the implementation and the tester, we develop a heuristic by biasing the search towards inputs that are promising in this game. We experimentally show that our heuristic accelerates the convergence of the Monte Carlo Tree Search algorithm, thus improving the performance of testing.

@techreport{2407.18994-SJMMN,
  author =              {Sankur, Ocan and J{\'e}ron, Thierry and Markey,
                         Nicolas and Mentr{\'e}, David and Noguchi, Reiya},
  title =               {Online Test Synthesis From Requirements: Enhancing
                         Reinforcement Learning with Game Theory},
  number =              {2407-18994},
  year =                {2024},
  month =               jul,
  doi =                 {10.48550/arXiv.2407-18994},
  institution =         {arXiv},
  abstract =            {We consider the automatic online synthesis of
                         black-box test cases from functional requirements
                         specified as automata for reactive implementations.
                         The goal of the tester is to reach some given state,
                         so as to satisfy a coverage criterion, while
                         monitoring the violation of the requirements. We
                         develop an approach based on Monte~Carlo Tree
                         Search, which is a classical technique in
                         reinforcement learning for efficiently selecting
                         promising inputs. Seeing the automata requirements
                         as a game between the implementation and the tester,
                         we develop a heuristic by biasing the search towards
                         inputs that are promising in this game.
                         We~experimentally show that our heuristic
                         accelerates the convergence of the Monte~Carlo Tree
                         Search algorithm, thus improving the performance of
                         testing.},
}