Hardness of Preorder Checking for Basic Formalisms

被引：1

作者：

Bozzelli, Laura ^{[1
]}

Legay, Axel ^{[1
]}

Pinchinat, Sophie ^{[1
]}

机构：

[1] IRISA, F-35042 Rennes, France

来源：

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING (LPAR-16) | 2010年 / 6355卷

关键词：

FINITE; SYSTEMS;

D O I：

10.1007/978-3-642-17511-4_8

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：119 / 135

页数：17

共 50 条

[31] Consistency Checking of Basic Cardinal Constraints over Connected Regions
Navarrete, Isabel
Morales, Antonio
Sciavicco, Guido
20TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2007, : 495 - 500
[32] Hardness and basic density variation in the juvenile wood of maritime pine
Dumail, JF
Castéra, P
Morlier, P
ANNALES DES SCIENCES FORESTIERES, 1998, 55 (08): : 911 - 923
[33] On the model checking problem for branching time logics and Basic Parallel Processes
Esparza, J
Kiehn, A
COMPUTER AIDED VERIFICATION, 1995, 939 : 353 - 366
[34] Attacks on the Basic cMix Design: On the Necessity of Commitments and Randomized Partial Checking
Galteland, Herman
Mjolsnes, Stig F.
Olimid, Ruxandra F.
PARADIGMS IN CRYPTOLOGY - MYCRYPT 2016: MALICIOUS AND EXPLORATORY CRYPTOLOGY, 2017, 10311 : 463 - 473
[35] Conformance Checking of Executed Clinical Guidelines in Presence of Basic Medical Knowledge
Bottrighi, Alessio
Chesani, Federico
Mello, Paola
Montali, Marco
Montani, Stefania
Terenziani, Paolo
BUSINESS PROCESS MANAGEMENT WORKSHOPS, PT II, 2012, 100 : 200 - +
[36] CHECKING OF RESULTS IN THE SURGICAL CLINIC BY EDP-CONTROLLED BASIC DOCUMENTATION
STOCK, W
MACKRODT, H
STANGL, T
DRESING, K
LANGENBECKS ARCHIV FUR CHIRURGIE, 1983, 361 : 906 - 906
[37] On the NP-Hardness of Checking Matrix Polytope Stability and Continuous-Time Switching Stability
Gurvits, Leonid
Olshevsky, Alexander
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2009, 54 (02) : 337 - 341
[38] MAINTENANCE, CHECKING AND REPAIR OF BASIC AGRICULTURAL IMPLEMENTS - THEMES AT THE AGRA-79
STRAUBE, K
KASPER, B
AGRARTECHNIK, 1979, 29 (06): : 274 - 276
[39] Improvement of Auto Checking Hardness Machine using Several Material Series of Aluminum Structural Frame: Case Study on Mitutoyo HR-522 Hardness Tester
Caesar, Bernardus Plasenta Previo
Istanto, Iwan
Pratama, Pandu Sandi
Cho, Joung Hyung
Prabowo, Aditya Rio
6TH INTERNATIONAL E-CONFERENCE ON INDUSTRIAL, MECHANICAL, ELECTRICAL AND CHEMICAL ENGINEERING (ICIMECE 2020) SPECIAL SYMPOSIUM - INTEGRITY OF MECHANICAL STRUCTURE AND MATERIAL, 2020, 27 : 117 - 124
[40] Handle Oscillations of a Pneumatic Hammer with Zero-Hardness of a Basic Elastic Element
Glushkov, Sergey
Pudovkin, Yuriy
VIII INTERNATIONAL SCIENTIFIC SIBERIAN TRANSPORT FORUM, VOL 1, 2020, 1115 : 756 - 767

← 1 2 3 4 5 →