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 条

[41] Basic Trends in Electronic Components Product Range Development: Radiation Hardness Aspects
Nikiforov, A. Y.
Boychenko, D. V.
Telets, V. A.
Smolin, A. A.
Elesin, V. V.
Ulanova, A. V.
Kessarinsky, L. N.
2017 IEEE 30TH INTERNATIONAL CONFERENCE ON MICROELECTRONICS (MIEL), 2017, : 45 - 48
[42] Basic principles of technological shaping of optical properties and radiation hardness of PWO crystals
Burachas, S
Beloglovsky, S
Elizarov, D
Makov, I
Saveliev, Y
Vassilieva, N
Ippolitov, M
Manko, V
Nikulin, S
Nyanin, A
Vasiliev, A
Apanasenko, A
Tamulaitis, G
RADIATION MEASUREMENTS, 2004, 38 (4-6) : 367 - 370
[43] The chemical hardness of molecules and the band gap of solids within charge equilibration formalisms Towards force field-based simulations of redox reactions
Mueser, M. H.
EUROPEAN PHYSICAL JOURNAL B, 2012, 85 (04):
[44] Synthesis-Aided Reliability Assurance of Basic Block Models for Model Checking Purposes
Buzhinsky, Igor
Pakonen, Antti
Vyatkin, Valeriy
2018 IEEE 27TH INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS (ISIE), 2018, : 669 - 674
[45] Label Cover Instances with Large Girth and the Hardness of Approximating Basic k-Spanner
Dinitz, Michael
Kortsarz, Guy
Raz, Ran
AUTOMATA, LANGUAGES, AND PROGRAMMING, ICALP 2012 PT I, 2012, 7391 : 290 - 301
[46] Label Cover Instances with Large Girth and the Hardness of Approximating Basic k-Spanner
Dinitz, Michael
Kortsarz, Guy
Raz, Ran
ACM TRANSACTIONS ON ALGORITHMS, 2016, 12 (02)
[47] DEVELOPMENT OF NOVEL DESIGN AND FRAME STRUCTURAL ASSESSMENT ON MITUTOYO'S AUTO CHECKING HARDNESS MACHINE USING REVERSE ENGINEERING APPROACH: SERIES HR-522 HARDNESS TESTER
Caesar, Bernandus Plasenta Previo
Hazimi, Hashfi
Sukanto, Heru
Prabowo, Aditya Rio
JOURNAL OF ENGINEERING SCIENCE AND TECHNOLOGY, 2020, 15 (02): : 1296 - 1318
[48] SPEC-CHECK - A BASIC PROGRAM FOR CHECKING THE INTERNAL CONSISTENCY OF COMPOSITE-MATERIALS SPECIFICATIONS
DARFLER, SC
BUYNY, RA
TOMORROWS MATERIALS : TODAY, BOOK 1 AND 2: 34TH INTERNATIONAL SAMPE SYMPOSIUM AND EXHIBITION, 1989, 34 : 667 - 677
[49] CHECKING THE REPRODUCIBILITY OF TEST-RESULTS - A BASIC ELEMENT IN METROLOGICAL QUALITY ASSURANCE FOR FUELS AND LUBRICANTS
KLOPOV, BN
SILIN, AV
ZHAVORONKIN, YA
MAKAROVA, NK
CHEMISTRY AND TECHNOLOGY OF FUELS AND OILS, 1982, 18 (3-4) : 187 - 189
[50] Basic cardiac life support providers checking the carotid pulse: Performance, degree of conviction, and influencing factors
Lapostolle, F
Le Toumelin, P
Agostinucci, JM
Catineau, J
Adnet, F
ACADEMIC EMERGENCY MEDICINE, 2004, 11 (08) : 878 - 880

← 1 2 3 4 5 →