Scholarlink

<p>In this work, we present <i>hypernode automata</i> as a specification formalism for hyperproperties of systems whose executions may be misaligned among themselves, such as concurrent systems. These automata consist of nodes labeled with <i>hypernode logic</i> formulas and transitions marked with synchronizing actions. Hypernode logic formulas establish relations between sequences of variable values among different system executions. This logic enables both synchronous and asynchronous analysis of traces. In its asynchronous view on execution traces, hypernode formulas establish relations on the order of value changes for each variable without correlating their timing. In both views, the analysis of different execution traces is synchronized through the transitions of hypernode automata. By combining logic’s declarative nature with automata’s procedural power, hypernode automata seamlessly integrate asynchronicity requirements at the node level with synchronicity between node transitions. We show that the model-checking problem for hypernode automata is decidable for specifications where each node specifies either a synchronous or an asynchronous requirement for the system’s executions, but not both.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Hypernode automata

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年12月9日

查看全文
  • Ezio Bartocci,
  • Marek Chalupa,
  • Thomas A. Henzinger,
  • Dejan Nickovic,
  • Ana Oliveira da Costa

摘要

In this work, we present hypernode automata as a specification formalism for hyperproperties of systems whose executions may be misaligned among themselves, such as concurrent systems. These automata consist of nodes labeled with hypernode logic formulas and transitions marked with synchronizing actions. Hypernode logic formulas establish relations between sequences of variable values among different system executions. This logic enables both synchronous and asynchronous analysis of traces. In its asynchronous view on execution traces, hypernode formulas establish relations on the order of value changes for each variable without correlating their timing. In both views, the analysis of different execution traces is synchronized through the transitions of hypernode automata. By combining logic’s declarative nature with automata’s procedural power, hypernode automata seamlessly integrate asynchronicity requirements at the node level with synchronicity between node transitions. We show that the model-checking problem for hypernode automata is decidable for specifications where each node specifies either a synchronous or an asynchronous requirement for the system’s executions, but not both.