Complexity analysis of a unifying algorithm for model checking interval temporal logic

This paper investigates the model checking issue of multirate hybrid systems. To this end, multirate automata are used to represent the possible behavior of multirate hybrid systems, and a dense timed interval temporal logic (DTITL) is defined to describe the desirable property. To check whether a multirate automaton satisfies a DTITL formula, a corresponding region automaton and a propositional interval temporal logic (PITL) formula are constructed. After each vertex of the region automaton being labeled with propositions appearing in the corresponding PITL formula, the model checking problem for mutirate hybrid systems is reduced to the same issue for PITL, which can be solved readily.

Download Full-text

Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2019/659 ◽

2019 ◽

Author(s):

Jakub Michaliszyn ◽

Piotr Witkowski

Keyword(s):

Model Checking ◽

Temporal Logic ◽

Order Logic ◽

Regular Expressions ◽

Multi Agent Systems ◽

Agent Systems ◽

Interval Temporal Logic ◽

Multi Agent ◽

Second Order Logic ◽

Monadic Second Order Logic

Epistemic Halpern-Shoham logic (EHS) is an interval temporal logic defined to verify properties of Multi-Agent Systems. In this paper we show that the model checking Multi-Agent Systems with regular expressions against the EHS specifications is decidable. We achieve this by reducing the model checking problem to the satisfiability problem of Monadic Second-Order Logic on trees.

Download Full-text

A Novel Approach for Intrusion Detection Based on Model Checking Interval Temporal Logic with Past Construct

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.680.451 ◽

2014 ◽

Vol 680 ◽

pp. 451-454

Author(s):

Peng Zhe Qiao ◽

Wei Jun Zhu

Keyword(s):

Model Checking ◽

Intrusion Detection ◽

Temporal Logic ◽

Pattern Matching ◽

New Method ◽

Network Attacks ◽

New Model ◽

Interval Temporal Logic ◽

Novel Approach ◽

Attack Models

Compared with the Intrusion Detection (ID) based on pattern matching, the model-checking-based methods can find the complex attacks. But their rates of missing report are still high. To solve this problem, we firstly use the Interval Temporal Logic with Past Construct (ITLPC) formulae to describe some signatures for network attacks. And then, we can use some automata to establish models of audit logs. On the basis of it, automata, i.e., attack models, and ITLPC formulae, i.e., signatures, constitute the two inputs of the ITLPC model checking algorithm. Therefore, a new model-checking-based ID algorithm is obtained by calling the ITLPC algorithm. Compared with the existing methods, the new method is more powerful, as shown in the experimental simulations.

Download Full-text