Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(5)
Computational Complexity
Finite State Machine
Model Checking
State Machine
Temporal Logic
Related Publications
(2)
Fixpoint Logics over Hierarchical Structures
Model Checking of Hierarchical State Machines
Subscribe
Academic
Publications
Verification of scopedependent hierarchical state machines
Verification of scopedependent hierarchical state machines,10.1016/j.ic.2008.03.017,Information and Computation/information and Control,Salvatore La
Edit
Verification of scopedependent hierarchical state machines
(
Citations: 4
)
BibTex

RIS

RefWorks
Download
Salvatore La Torre
,
Margherita Napoli
,
Mimmo Parente
,
Gennaro Parlato
A hierarchical
state machine
(Hsm) is a
finite state machine
where a vertex can either expand to another hierarchical
state machine
(box) or be a basic vertex (node). Each node is labeled with atomic propositions. We study an extension of such model which allows atomic propositions to label also boxes (Shsm). We show that Shsms can be exponentially more succinct than Shsms and verification is in general harder by an exponential factor. We carefully establish the
computational complexity
of reachability, cycle detection, and
model checking
against general Ltl and Ctl specifications. We also discuss some natural and interesting restrictions of the considered problems for which we can prove that Shsms can be verified as much efficiently as Hsms, still preserving an exponential gap of succinctness.
Journal:
Information and Computation/information and Control  IANDC
, vol. 206, no. 910, pp. 11611177, 2008
DOI:
10.1016/j.ic.2008.03.017
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.sciencedirect.com
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
(
linkinghub.elsevier.com
)
More »
Citation Context
(3)
...The work since then was focused on recursive systems, with the exception of [12,
16
,18]...
Benjamin Aminof
,
et al.
Improved Model Checking of Hierarchical Systems
...A hierarchical model uses as nodes both ordinary nodes or supernodes, which are models themselves [AY01,ABE+05,
LNPP08
]...
...labeled with atomic propositions [
LNPP08
])...
Aniello Murano
,
et al.
Program Complexity in Hierarchical Module Checking
...The work since then was focused on recursive systems, with the exception of [12,
17
, 20]...
Benjamin Aminof
,
et al.
Improved Model Checking of Hierarchical SystemsI
References
(8)
Computeraided verification
(
Citations: 173
)
E. M. Clarke
,
R. P. Kurshan
Journal:
IEEE Spectrum
, vol. 33, no. 6, pp. 6167, 1996
The Unified Modeling Language User Guide
(
Citations: 3813
)
Grady Booch
,
James E. Rumbaugh
,
Ivar Jacobson
Journal:
Journal of Database Management  JDM
, vol. 10, no. 4, pp. 5152, 1999
Objectoriented Modeling and Design
(
Citations: 4266
)
James E. Rumbaugh
,
Michael R. Blaha
,
William J. Premerlani
,
Frederick Eddy
,
William E. Lorensen
Published in 1991.
Realtime object oriented modeling and design
(
Citations: 68
)
B. Selic
,
G. Gullekson
,
P. T. Ward
Published in 1994.
Model checking of hierarchical state machines
(
Citations: 43
)
Rajeev Alur
,
Mihalis Yannakakis
Journal:
ACM Transactions on Programming Languages and Systems  TOPLAS
, vol. 23, no. 3, pp. 273303, 2001
Sort by:
Citations
(4)
Improved Model Checking of Hierarchical Systems
Benjamin Aminof
,
Orna Kupferman
,
Aniello Murano
Conference:
Verification, Model Checking and Abstract Interpretation  VMCAI
, pp. 6177, 2010
Program Complexity in Hierarchical Module Checking
(
Citations: 2
)
Aniello Murano
,
Margherita Napoli
,
Mimmo Parente
Conference:
Logic Programming and Automated Reasoning/Russian Conference on Logic Programming  LPAR(RCLP)
, pp. 318332, 2008
Software life cycle modelsindustrial implications
(
Citations: 1
)
V. Kadary
,
D. EvenTsur
,
N. Halperin
,
S. Koenig
Conference:
Israel Conference on Computer Systems and Software Engineering  ICCSSE
, 1989
Improved Model Checking of Hierarchical SystemsI
Benjamin Aminof
,
Orna Kupferman
,
Aniello Murano