@mastersthesis{Schwoon98,
author = {Schwoon, Stefan},
title = {{\"U}bersetzung von {SDL}-Spezifikationen in {P}etri-Netze},
school = {Universit{\"a}t Hildesheim},
year = {1998},
month = aug,
type = {{M}aster's {T}hesis},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/schwoon98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/schwoon98.ps},
otherurl = {http://theoretica.informatik.uni-oldenburg.de/~pep/},
abstract = {It is shown how to translate formal specifications written in SDL
into Petri nets. A compiler is implemented and integrated into
the PEP-project. To allow verifications of SDL-specifications,
the compiler is supplemented by a reference component and a
formula transformer.},
lsv-lang = {DE}
}
@inproceedings{EHRS-cav00,
address = {Chicago, Illinois, USA},
month = jul,
year = 2000,
volume = 1855,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Emerson, E. Allen and Sistla, A. Prasad},
acronym = {{CAV} 2000},
booktitle = {{P}roceedings of the 12th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV} 2000)},
author = {Esparza, Javier and Hansel, David
and Rossmanith, Peter and Schwoon, Stefan},
title = {Efficient Algorithms for Model Checking Pushdown Systems},
pages = {232-247},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ehrs-cav00.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ehrs-cav00.ps},
abstract = {We study model checking problems for pushdown systems and linear
time logics. We show that the global model checking problem
(computing the set of configurations, reachable or not, that
violate the formula) can be solved in \(O(g_P^3\cdot g_B^3)\) time and
\(O(g_P^2\cdot g_B^2)\) space, where \(g_P\) and \(g_B\) are the size of
the pushdown system and the size of a B{\"u}chi automaton for
the negation of the formula. The global model checking problem
for reachable configurations can be solved in \(O(g_P^4\cdot g_B^3)\)
time and \(O(g_P^4\cdot g_B^2)\) space. In~the case of pushdown systems
with constant number of control states (relevant for our
application), the complexity becomes \(O(g_P\cdot g_B^3)\) time and
\(O(g_P\cdot g_B^2)\) space and \(O(g_P^2\cdot g_B^3)\) time and
\(O(g_P^2\cdot g_B^2)\) space, respectively. We show applications of
these results in the area of program analysis and present some
experimental results.}
}
@article{ERS-beatcs00,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Esparza, Javier and Rossmanith, Peter and Schwoon, Stefan},
title = {A Uniform Framework for Problems on Context-Free Grammars},
volume = {72},
pages = {169-177},
month = oct,
year = {2000},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ehr-beatcs00.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ehr-beatcs00.ps},
abstract = {Bouajjani and others presented an automata-based approach to a
number of elementary problems on context-free grammars. This
approach is of pedagogical interest since it provides a
uniform solution to decision procedures usually solved by
independent algorithms in textbooks. This~paper improves upon
previous work in a number of ways. We~present a new algorithm
which not only has a better space complexity but is also
(in~our opinion) easier to read and understand. Moreover,
a~closer inspection reveals that the new algorithm is
competitive to well-known solutions for most (but not~all)
standard problems.}
}
@inproceedings{EKS-tacs01,
address = {Sendai, Japan},
month = oct,
year = 2001,
volume = 2215,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Kobayashi, Naoki and Pierce, Benjamin C.},
acronym = {{TACS}'01},
booktitle = {{P}roceedings of the 4th {I}nternational
{W}orkshop on {T}heoretical {A}spects of
{C}omputer {S}oftware
({TACS}'01)},
author = {Esparza, Javier and Ku\v{c}era, Anton\'{\i}n and Schwoon, Stefan},
title = {Model-Checking {LTL} with Regular Valuations
for Pushdown Systems},
pages = {306-339},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/eks-tacs01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/eks-tacs01.ps},
abstract = {Recent works have proposed pushdown systems as a tool for
analyzing programs with (recursive) procedures. In particular,
the model-checking problem for LTL has been studied. In this
paper we examine an extension of this, namely model-checking
with regular valuations. The problem is solved via two different
techniques, with an eye on efficiency both techniques can be
shown to be essentially optimal. Our methods are applicable to
problems in different areas, \textit{e.g.}, data-flow analysis, analysis
of systems with checkpoints, \textit{etc.}, and provide a general,
unifying and efficient framework for solving these problems.}
}
@inproceedings{ES-cav01,
address = {Paris, France},
month = jul,
year = 2001,
volume = 2102,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
acronym = {{CAV}'01},
booktitle = {{P}roceedings of the 13th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'01)},
author = {Esparza, Javier and Schwoon, Stefan},
title = {A {BDD}-based Model Checker for Recursive Programs},
pages = {324-336},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/es-cav01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/es-cav01.ps},
abstract = {We present a model-checker for boolean programs with (possibly
recursive) procedures and the temporal logic~LTL. The~checker
is guaranteed to terminate even for (usually faulty) programs
in which the depth of the recursion is not bounded. The
algorithm uses automata to finitely represent possibly infinite
sets of stack contents and BDDs to compactly represent finite
sets of values of boolean variables. We illustrate the checker
on some examples and compare it with the Bebop tool of Ball
and Rajamani.}
}
@incollection{Sch02a,
missingmonth = mar,
missingnmonth = 3,
year = 2002,
volume = 2500,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gr{\"a}del, Erich and Thomas, Wolfgang and Wilke, Thomas},
acronym = {{A}utomata, {L}ogics, and {I}nfinite {G}ame},
booktitle = {{A}utomata, {L}ogics, and {I}nfinite {G}ame: {A}~{G}uide to
{C}urrent {R}esearch},
author = {Schwoon, Stefan},
title = {Determinization and Complementation of {S}treett Automata},
pages = {79-91},
abstract = {Streett automata are automata on infinite words. They differ
from other formalisms in their acceptance condition which
models strong fairness constraints. Again, their expressiveness
is equal to that of B{\"u}chi automata; however, Streett automata
can have an exponentially more succinct representation for
certain properties. Here, we survey results about upper
and lower bounds on the problems of determinization and
complementation of Streett automata.}
}
@phdthesis{schwoon-phd02,
author = {Schwoon, Stefan},
title = {Model-Checking Pushdown Systems},
school = {Technische Universit{\"a}t M{\"u}nchen},
year = {2002},
month = jun,
type = {{Ph.}{D.} {T}hesis},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schwoon-phd02.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schwoon-phd02.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/schwoon-phd02.ps},
abstract = {The thesis investigates an approach to automated software
verification based on pushdown systems. Pushdown systems are,
roughly speaking, transition systems whose states include a
stack of unbounded length; there is a natural correspondence
between them and the execution sequences of programs with
(possibly recursive) subroutines. The thesis examines
model-checking problems for pushdown systems, improving
previously known algorithms in terms of both asymptotic
complexity and practical usability. The improved algorithms are
used in a tool called Moped. The tool acts as a model-checker
for linear-time logic (LTL) on pushdown systems. Two different
symbolic techniques are combined to make the model-checking
feasible: automata-based techniques are used to handle
infinities raised by a program's control, and Binary Decision
Diagrams (BDDs) to combat the state explosion raised by its
data. It is shown how the resulting system can be used to verify
properties of algorithms with recursive procedures by means of
several examples. The checker has also been used on
automatically derived abstractions of some large C programs.
Moreover, the thesis investigates several optimizations which
served to improve the efficiency of the checker.}
}
@inproceedings{SSE-tools02,
address = {Brno, Czech Republic},
month = aug,
year = 2002,
howpublished = {Technical Report FIMU-RS-2002-05,
Masaryk University, Brno, Czech Republic},
publisher = {Uppsala University},
editor = {{\v C}ern{\'a}, Ivana},
noacronym = {},
booktitle = {{P}roceedings of the {T}ools {D}ay {W}orkshop},
author = {Schr{\"o}ter, Claus and Schwoon, Stefan and Esparza, Javier},
title = {The Model-Checking Kit},
pages = {22-31},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sse-tools02.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sse-tools02.ps},
abstract = {The Model-Checking Kit is a collection of programs
which allow to model finite state systems using a variety of
modelling languages, and verify them using a variety of
checkers, including deadlock-checkers, reachability-checkers,
and model-checkers for the temporal logics CTL and~LTL.}
}
@article{BHKS-beatcs03,
publisher = {European Association for
Theoretical Computer Science},
journal = {EATCS Bulletin},
author = {Brauer, Wilfried and Holzer, Markus and
K{\"o}nig, Barbara and Schwoon, Stefan},
title = {The Theory of Finite-State Adventures},
year = {2003},
volume = {79},
pages = {230-237},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHKS-beatcs03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHKS-beatcs03.ps},
abstract = {The study of finite-state adventures, abbreviated by FSA, is a
topic that has, despite its origins that can be traced back to
medieval times, been neglected in the relevant literature. We
attempt to close this gap and give a full account of a
five-level hierarchy of finite-state adventures.}
}
@article{EKS-icomp03,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Esparza, Javier and Ku{\v c}era, Anton{\'\i}n and Schwoon, Stefan},
title = {Model-Checking {LTL} with Regular Valuations
for Pushdown Systems},
month = nov,
year = {2003},
volume = {186},
number = {2},
pages = {355-376},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/eks-icomp03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/eks-icomp03.ps},
abstract = {Recent works have proposed pushdown systems as a tool for
analyzing programs with (recursive) procedures, and the
model-checking problem for LTL has received special attention.
However, all these works impose a strong restriction on the
possible valuations of atomic propositions: whether a
configuration of the pushdown system satisfies an atomic
proposition or not can only depend on the current control
state of the pushdown automaton and on its topmost stack symbol.
In this paper we consider LTL with regular valuations: the set
of configurations satisfying an atomic proposition can be an
arbitrary regular language. The model-checking problem is solved
via two different techniques, with an eye on efficiency. The
resulting algorithms are polynomial in certain measures of the
problem which are usually small, but can be exponential in the
size of the problem instance. However, we show that this
exponential blowup is inevitable. The extension to regular
valuations allows to model problems in different areas; for
instance, we show an application to the analysis of systems
with checkpoints. We claim that our model-checking algorithms
provide a general, unifying and efficient framework for solving
them.}
}
@inproceedings{RSJ-sas03,
address = {San~Diego, California, USA},
month = jun,
year = 2003,
volume = 2694,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cousot, Radhia},
acronym = {{SAS}'03},
booktitle = {{P}roceedings of the 10th {I}nternational {S}ymposium
{S}tatic {A}nalysis ({SAS}'03)},
author = {Reps, Thomas and Schwoon, Stefan and Jha, Somesh},
title = {Weighted Pushdown Systems and Their Application
to Interprocedural Dataflow Analysis},
pages = {189-213},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rsj-sas03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rsj-sas03.ps},
abstract = {Recently, pushdown systems (PDSs) have been extended to weighted
PDSs, in which each transition is labeled with a value, and the
goal is to determine the meet-over-allpaths value (for paths
that meet a certain criterion). This paper shows how weighted
PDSs yield new algorithms for certain classes of interprocedural
dataflow-analysis problems.}
}
@inproceedings{SJRS-csfw03,
address = {Pacific Grove, California, USA},
month = jun # {-} # jul,
year = 2003,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSFW}'03},
booktitle = {{P}roceedings of the
16th {IEEE} {C}omputer {S}ecurity {F}oundations
{W}orkshop ({CSFW}'03)},
author = {Schwoon, Stefan and Jha, Somesh
and Reps, Thomas and Stubblebine, Stuart},
title = {On Generalized Authorization Problems},
pages = {202-218},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sjrs-csfw03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/sjrs-csfw03.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sjrs-csfw03.ps},
abstract = {This paper defines a framework in which one can formalize a
variety of authorization and policy issues that arise in access
control of shared computing resources. Instantiations of the
framework address such issues as privacy, recency, validity,
and trust. The paper presents an efficient algorithm for solving
all authorization problems in the framework; this approach
yields new algorithms for a number of specific authorization
problems.}
}
@inproceedings{SSE-atpn03,
address = {Eindhoven, The Netherlands},
month = jun,
year = 2003,
volume = 2679,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van der Aalst, Wil M. P. and Best, Eike},
acronym = {{ICATPN}'03},
booktitle = {{P}roceedings of the 24th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({ICATPN}'03)},
author = {Schr{\"o}ter, Claus and Schwoon, Stefan and Esparza, Javier},
title = {The Model-Checking Kit},
pages = {463-472},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sse-atpn03.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sse-atpn03.ps},
abstract = {The Model-Checking Kit is a collection of programs which allow
to model finite state systems using a variety of modelling
languages, and verify them using a variety of checkers,
including deadlock-checkers, reachability-checkers, and
model-checkers for the temporal logics CTL and LTL.}
}
@article{HS-tcs04,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Holzer, Markus and Schwoon, Stefan},
title = {Assembling Molecules in {A}tomix is Hard},
year = {2004},
month = feb,
volume = {303},
number = {3},
pages = {447-462},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hs-tcs04.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/hs-tcs04.pdf},
abstract = {It is shown that assembling molecules in the Atomix game can be
used to simulate finite automata. In particular, an instance of
Atomix is constructed that has a solution if and only if the
non-emptiness intersection problem for finite automata is
solvable. This shows that the game under consideration is
PSPACE-complete, improving a recent result of H{\"u}ffner \textit{et~al.}
Thus, there are Atomix games which have superpolynomially long
optimal solutions. We also give an easy construction of Atomix
game levels whose optimal solutions meet the worst case.}
}
@inproceedings{HS-fun04,
address = {Isola d'Elba, Italy},
month = may,
year = 2004,
publisher = {Edizioni Plus, Universit{\`a} di Pisa},
editor = {Ferragina, Paolo and Grossi, Roberto},
acronym = {{FUN}'04},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {F}un with {A}lgorithms
({FUN}'04)},
author = {Holzer, Markus and Schwoon, Stefan},
title = {Reflections on {R}eflexion~-- Computational Complexity
Considerations on a Puzzle Game},
pages = {90-105},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/hs-fun04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/hs-fun04.ps},
abstract = {We investigate the complexity of solving puzzles in the game
Reflexion. It is shown that the difficulty of the puzzles
depends critically on the features used in the puzzles; the
most basic variant of the game is SL-complete, and hence can be
solved in polynomial time, whereas other variants are NP- or
even PSPACE-complete.}
}
@inproceedings{BESS-fsttcs05,
address = {Hyderabad, India},
month = dec,
year = 2005,
volume = 3821,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ramanujam, R. and Sen, Sandeep},
acronym = {{FSTTCS}'05},
booktitle = {{P}roceedings of the 25th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'05)},
author = {Bouajjani, Ahmed and Esparza, Javier
and Schwoon, Stefan and Strej\v{c}ek, Jan},
title = {Reachability analysis of multithreaded software
with asynchronous communication},
pages = {348-359},
doi = {10.1007/11590156_28},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bess-fsttcs05.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/bess-fsttcs05.ps},
abstract = {We introduce asynchronous dynamic pushdown networks (ADPN),
a new model for multithreaded programs in which pushdown
systems communicate via shared memory. ADPN generalizes both
CPS (concurrent pushdown systems) and DPN (dynamic pushdown
networks). We show that ADPN exhibit several advantages as
a program model. Since the reachability problem for ADPN
is undecidable even in the case without dynamic creation
of processes, we address the \emph{bounded} reachability
problem, which considers only those computation sequences
where the (index of the) thread accessing the shared memory
is changed at most a fixed given number of times. We provide
efficient algorithms for both forward and backward reachability
analysis. The algorithms are based on automata techniques for
symbolic representation of sets of configurations.}
}
@inproceedings{EGS-sas05,
address = {London, UK},
month = sep,
year = 2005,
volume = 3672,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hankin, Chris and Siveroni, Igor},
acronym = {{SAS}'05},
booktitle = {{P}roceedings of the 12th {I}nternational {S}ymposium
{S}tatic {A}nalysis ({SAS}'05)},
author = {Esparza, Javier and Ganty, Pierre and Schwoon, Stefan},
title = {Locality-Based Abstractions},
pages = {118-134},
doi = {10.1007/11547662_10},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/egs-sas05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/egs-sas05.pdf},
abstract = {We present locality-based abstractions, in which a set of states
of a distributed system is abstracted to the collection of views
that some observers have of the states. Special cases of
locality-abstractions have been used in different contexts
(planning, analysis of concurrent programs, concurrency theory).
In this paper we give a general definition in the context of
abstract interpretation, show that arbitrary locality-based
abstractions are hard to compute in general, and provide two
solutions to this problem. The solutions are evaluated in
several case studies.}
}
@article{RSJM-scp05,
publisher = {Elsevier Science Publishers},
journal = {Science of Computer Programming},
author = {Reps, Thomas and Schwoon, Stefan and Jha, Somesh and Melski, David},
title = {Weighted Pushdown Systems and Their Application
to Interprocedural Dataflow Analysis},
volume = {58},
number = {1-2},
pages = {206-263},
month = oct,
year = {2005},
doi = {10.1016/j.scico.2005.02.009},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rsjm-scp05.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/rsjm-scp05.ps},
abstract = {Recently, pushdown systems (PDSs) have been extended to weighted
PDSs, in which each transition is labeled with a value, and the goal is to
determine the meet-over-all-paths value (for paths that meet a certain
criterion). This paper shows how weighted PDSs yield new algorithms for
certain classes of interprocedural dataflow-analysis problems.}
}
@inproceedings{SE-tacas05,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 2005,
volume = 3440,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halbwachs, Nicolas and Zuck, Lenore D.},
acronym = {{TACAS}'05},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'05)},
author = {Schwoon, Stefan and Esparza, Javier},
title = {A Note on On-The-Fly Verification Algorithms},
pages = {174-190},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/se-tacas05.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/se-tacas05.ps},
abstract = {The automata-theoretic approach to LTL verification relies on an
algorithm for finding accepting cycles in a B{\"u}chi automaton.
Explicit-state model checkers typically construct the automaton
``on~the~fly'' and explore its states using depth-first search.
We survey algorithms proposed for this purpose and identify
two good algorithms, a new algorithm based on nested DFS, and
another based on strongly connected components. We compare
these algorithms both theoretically and experimentally and
determine cases where both algorithms can be useful.}
}
@inproceedings{SSE-tacas05,
address = {Edinburgh, Scotland, UK},
month = apr,
year = 2005,
volume = 3440,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halbwachs, Nicolas and Zuck, Lenore D.},
acronym = {{TACAS}'05},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'05)},
author = {Suwimonteerabuth, Dejvuth and Schwoon, Stefan and Esparza, Javier},
title = {{jM}oped: A~{J}ava bytecode checker based on {M}oped},
pages = {541-545},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sse-tacas05.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/sse-tacas05.ps},
abstract = {We present a tool for finding errors in Java programs that
translates Java bytecodes into symbolic pushdown systems,
which are then checked by the Moped tool.}
}
@inproceedings{EKS-tacas06,
address = {Vienna, Austria},
month = mar,
year = 2006,
volume = {3920},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hermanns, Holger and Palsberg, Jens},
acronym = {{TACAS}'06},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'06)},
author = {Javier Esparza and Stefan Kiefer and Stefan Schwoon},
title = {Abstraction Refinement with {C}raig Interpolation and Symbolic
Pushdown Systems},
pages = {489-503},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EKS-tacas06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EKS-tacas06.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EKS-tacas06.ps},
doi = {10.1007/11691372_35},
abstract = {Counterexample-guided abstraction refinement (CEGAR) has proven
to be a powerful method for software model-checking. In this
paper, we investigate this concept in the context of
sequential (possibly recursive) programs whose statements are
given as BDDs. We examine how Craig interpolants can be
computed efficiently in this case and propose a new, special
type of interpolants. Moreover, we show how to treat multiple
counterexamples in one refinement cycle. We have implemented
this approach within the model-checker Moped and report on
experiments.}
}
@inproceedings{JSWR-tacas06,
address = {Vienna, Austria},
month = mar,
year = 2006,
volume = {3920},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Hermanns, Holger and Palsberg, Jens},
acronym = {{TACAS}'06},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'06)},
author = {Jha, Somesh and Schwoon, Stefan and Wang, Hao and Reps, Thomas},
title = {Weighted Pushdown Systems and Trust-Management Systems},
pages = {1-26},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JSWR-tacas06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JSWR-tacas06.pdf},
doi = {10.1007/11691372_1},
abstract = {The authorization problem is to decide whether, according to
a security policy, some principal should be allowed access
to a resource. In the trust-management system SPKI/SDSI, the
security policy is given by a set of certificates, and proofs
of authorization take the form of certificate chains. The
certificate-chain-discovery problem is to discover a proof of
authorization for a given request. Certificate-chain-discovery
algorithms for SPKI/SDSI have been investigated by several
researchers. We consider a variant of the certificate-chain
discovery problem where the certificates are distributed
over a number of servers, which then have to cooperate to
identify the proof of authorization for a given request. We
propose two protocols for this purpose. These protocols are
based on distributed model-checking algorithms for weighted
pushdown systems (WPDSs). These protocols can also handle
cases where certificates are labeled with weights and where
multiple certificate chains must be combined to form a proof
of authorization. We have implemented these protocols in a
prototype and report preliminary results of our evaluation.}
}
@inproceedings{NSRL-fmse06,
address = {Alexandria, Virginia, USA},
month = nov,
year = 2006,
publisher = {ACM Press},
editor = {Gordon, Andrew D. and Sands, David},
acronym = {{FMSE}'06},
booktitle = {{P}roceedings of the 4th {ACM} {W}orkshop on {F}ormal {M}ethods
in {S}ecurity {E}ngineering ({FMSE}'06)},
author = {Naldurg, Prasad and Schwoon, Stefan
and Rajamani, Sriram and Lambert, John},
title = {{NETRA}: Seeing Through Access Control},
pages = {55-66},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NSRL-fmse06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/NSRL-fmse06.pdf},
doi = {10.1145/1180337.1180343},
abstract = {We present \textsc{netra}, a tool for systematically analyzing
and detecting explicit information-flow vulnerabilities in access-control
configurations. Our tool takes a snapshot of the access-control metadata,
and performs static analysis on this snapshot. We devise an augmented
relational calculus that naturally models both access control mechanisms
and information-flow policies uniformly. This calculus is interpreted as a
logic program, with a fixpoint semantics similar to Datalog, and produces
all access tuples in a given configuration that violate properties of
interest. Our analysis framework is programmable both at the model level
and at the property level, effectively separating mechanism from policy.
We demonstrate the effectiveness of this modularity by analyzing two
systems with very different mechanisms for access control--Windows XP and
SELinux--with the same specification of information-flow vulnerabilities.
\textsc{netra} finds vulnerabilities in default configurations of both
systems.}
}
@inproceedings{SSE-atva06,
address = {Beijing, China},
month = oct,
year = {2006},
volume = 4218,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Graf, Susanne and Zhang, Wenhui},
acronym = {{ATVA}'06},
booktitle = {{P}roceedings of the 4th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'06)},
author = {Suwimonteerabuth, Dejvuth and Schwoon, Stefan and Esparza, Javier},
title = {Efficient Algorithms for Alternating Pushdown Systems
with an Application to the Computation of Certificate Chains},
pages = {141-153},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SSE-atva06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SSE-atva06.pdf},
doi = {10.1007/11901914_13},
abstract = {Motivated by recent applications of pushdown systems
to computer security problems, we present an efficient
algorithm for the reachability problem of alternating
pushdown systems. Although the algorithm is exponential,
a careful analysis reveals that the exponent is usually
small in typical applications. We show that the algorithm
can be used to compute winning regions in pushdown games.
In a second contribution, we observe that the algorithm
runs in polynomial time for a certain subproblem, and show
that the computation of certificate chains with threshold
certificates in the SPKI/SDSI authorization framework can be
reduced to this subproblem. We present a detailed complexity
analysis of the algorithm and its application, and report on
experimental results obtained with a prototype implementation.}
}
@inproceedings{WJRSS-esorics06,
address = {Hamburg, Germany},
month = sep,
year = 2006,
volume = 4189,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gollmann, Dieter and Meier, Jan and Sabelfeld, Andrei},
acronym = {{ESORICS}'06},
booktitle = {{P}roceedings of the 11th {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'06)},
author = {Wang, Hao and Jha, Somesh and Reps, Thomas
and Schwoon, Stefan and Stubblebine, Stuart},
title = {Reducing the Dependence of {SPKI}{\slash}{SDSI} on~{PKI}},
pages = {156-173},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/WJRSS-esorics06.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/WJRSS-esorics06.pdf},
doi = {10.1007/11863908_11},
abstract = {Trust-management systems address the authorization problem in
distributed systems. They offer several advantages over other approaches,
such as support for delegation and making authorization decisions in a
decentralized manner. Nonetheless, trust-management systems such as
KeyNote and SPKI\slash SDSI have seen limited deployment in the real
world. One reason for this is that both systems require a public-key
infrastructure~(PKI) for authentication, and PKI has proven difficult to
deploy, because each user is required to manage his\slash her own
private\slash public key pair. The key insight of our work is that
issuance of certificates in trust-management systems, a task that usually
requires public-key cryptography, can be achieved using secret-key
cryptography as well. We~demonstrate this concept by showing how
SPKI\slash SDSI can be modified to use Kerberos, a~secret-key based
authentication system, to~issue SPKI\slash SDSI certificates.
The~resulting trust-management system retains all the capabilities of
SPKI\slash SDSI, but is much easier to use because a public key is only
required for each SPKI\slash SDSI server, but no longer for every user.
Moreover, because Kerberos is already well established, our~approach makes
SPKI\slash SDSI-based trust management systems easier to deploy in the
real world.}
}
@inproceedings{SBSE-cav07,
address = {Berlin, Germany},
month = jul,
year = 2007,
volume = 4590,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Damm, Werner and Hermanns, Holger},
acronym = {{CAV}'07},
booktitle = {{P}roceedings of the 19th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'07)},
author = {Suwimonteerabuth, Dejvuth and Berger, Felix
and Schwoon, Stefan and Esparza, Javier},
title = {j{M}oped: A~Test Environment for {J}ava programs},
pages = {164-167},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SBSE-cav07.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SBSE-cav07.ps},
doi = {10.1007/978-3-540-73368-3_19},
abstract = {We present jMoped, a test environment for Java programs. Given a
Java method, jMoped can simulate its execution for all possible arguments
within a finite range and generate coverage information for these
executions. Moreover, it~checks for some common Java errors, i.e.
assertion violations, null pointer exceptions, and array bound violations.
When an error is found, jMoped finds out the arguments that lead to the
error. A~JUnit test case can also be automatically generated for further
testing.}
}
@inproceedings{BCKS-ufo07,
address = {Siedlce, Poland},
month = jun,
year = 2007,
publisher = {Publishing House of University of Podlasie},
editor = {Fabre, {\'E}ric and Khomenko, Victor},
acronym = {{UFO}'07},
booktitle = {{P}roceedings of the {W}orkshop on {U}n{FO}lding and partial order
techniques ({UFO}'07)},
author = {Baldan, Paolo and Corradini, Andrea
and K{\"o}nig, Barbara and Schwoon, Stefan},
title = {{M}c{M}illan's complete prefix for contextual nets},
pages = {32-49},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCKS-ufo07.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCKS-ufo07.ps},
abstract = {In a seminal paper, McMillan proposed a technique for
constructing a finite complete prefix of the unfolding of bounded (i.e.,
finite-state) Petri nets, which can be used for verification purposes.
Contextual nets are a generalisation of Petri nets suited to model systems
with read-only access to resources. When working with contextual nets, a
finite complete prefix can be obtained by applying McMillan's construction
to a suitable encoding of the contextual net into an ordinary net.
However, it has been observed that if the unfolding is itself a contextual
net, then the complete prefix can be significantly smaller than the one
obtained with the above technique. A construction for generating such a
contextual complete prefix has been proposed for a special class of nets,
called read-persistent. In this paper we propose a new algorithm that
works for arbitrary semi-weighted, bounded contextual nets. The
construction explicitly takes into account the fact that, unlike ordinary
or read-persistent nets, an event can have several different histories in
contextual net computations. }
}
@article{EKS-sttt08,
publisher = {Springer},
journal = {International Journal on Software Tools
for Technology Transfer},
author = {Esparza, Javier and Kanade, Pradeep and Schwoon, Stefan},
title = {A Negative Result on Depth-First Unfoldings},
volume = {10},
number = {2},
year = {2008},
pages = {161-166},
month = mar,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EKS-sttt08.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EKS-sttt08.ps},
doi = {10.1007/s10009-007-0030-5}
}
@inproceedings{BESS-tacas08,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = {4963},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ramakrishnan, C. R. and Rehof, Jakob},
acronym = {{TACAS}'08},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'08)},
author = {Bouajjani, Ahmed and Esparza, Javier
and Schwoon, Stefan and Suwimonteerabuth, Dejvuth},
title = {{SDSI}rep: A~Reputation System based on~{SDSI}},
pages = {501-516},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BESS-tacas08.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BESS-tacas08.ps},
doi = {10.1007/978-3-540-78800-3_39},
abstract = {We introduce SDSIrep, a reputation system based on the
SPKI/SDSI authorization system. It~is well-known that a
system of SPKI/SDSI certificates corresponds to the formal
model of a pushdown system~(PDS). Our~system, SDSIrep,
allows principals to express trust and recommendations in the
form of so-called certificates with weights. By interpreting
weights as probabilities, we obtain a random-walk model of
the reputation of a principal. Thus, SDSIrep represents an
application of the theory of probabilistic PDSs to the field
of computer security. We present an algorithm to compute the
reputation of each principal. An extension of SDSIrep
also provides for so-called intersection certificates,
by which, loosely speaking, a principal gains reputation if
recommended by all members of a given group of principals. On
a formal-methods level, this extension makes SDSIrep
correspond to probabilistic alternating PDSs, and we extend
the underlying theory of PDSs to handle this case. As an
example we sketch a small academic reputation system that
combines information from different reputation sources,
like conferences, coauthors, and rankings.}
}
@incollection{BCKS-topnoc08,
month = nov,
year = 2008,
volume = 5100,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
booktitle = {Transactions on {P}etri Nets and Other Models of Concurrency~{I}},
author = {Baldan, Paolo and Corradini, Andrea
and K{\"o}nig, Barbara and Schwoon, Stefan},
title = {{M}c{M}illan's complete prefix for contextual nets},
pages = {199-220},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCKS-topnoc08.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BCKS-topnoc08.ps},
doi = {10.1007/978-3-540-89287-8_12},
abstract = {In a seminal paper, McMillan proposed a technique for
constructing a finite complete prefix of the unfolding of bounded (i.e.,
finite-state) Petri nets, which can be used for verification purposes.
Contextual nets are a generalisation of Petri nets suited to model systems
with read-only access to resources. When working with contextual nets, a
finite complete prefix can be obtained by applying McMillan's construction
to a suitable encoding of the contextual net into an ordinary net.
However, it has been observed that if the unfolding is itself a contextual
net, then the complete prefix can be significantly smaller than the one
obtained with the above technique. A construction for generating such a
contextual complete prefix has been proposed for a special class of nets,
called read-persistent. In this paper, we propose an algorithm that works
for arbitrary semi-weighted, bounded contextual nets. The construction
explicitly takes into account the fact that, unlike in ordinary or
read-persistent nets, an event can have several different histories in
general contextual net computations.}
}
@inproceedings{SES-spin08,
address = {Los Angeles, California, USA},
month = aug,
year = 2008,
volume = 5156,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Havelund, Klaus and Majumdar, Rupak and Palsberg, Jens},
acronym = {{SPIN}'08},
booktitle = {{P}roceedings of the 15th {I}nternational
{SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware
({SPIN}'08)},
author = {Suwimonteerabuth, Dejvuth and Esparza, Javier and Schwoon, Stefan},
title = {Symbolic Context-Bounded Analysis
of Multithreaded {J}ava Programs},
pages = {270-287},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SES-spin08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SES-spin08.pdf},
doi = {10.1007/978-3-540-85114-1_19},
abstract = {The reachability problem is undecidable for programs with both
recursive procedures and multiple threads with shared memory.
Approaches to this problem have been the focus of much recent
research. One of these is to use context-bounded reachability,
i.e. to consider only those runs in which the active thread
changes at most \(k\)~times, where \(k\)~is fixed. However, to the
best of our knowledge, context-bounded reachability has not
been implemented in any tool so far, primarily because its
worst-case runtime is prohibitively high, i.e. \(O(n^{k})\), where
\(n\)~is the size of the shared memory. Moreover, existing
algorithms for context-bounded reachability do not admit a
meaningful symbolic implementation (e.g., using BDDs) to reduce
the run-time in practice. In this paper, we propose an
improvement that overcomes this problem. We have implemented
our approach in the tool jMoped and report on experiments.}
}
@article{EKS-jsat08,
publisher = {Delft University and {IOS} Press},
journal = {Journal on Satisfiability, Boolean Modeling and Computation},
author = {Esparza, Javier and Kiefer, Stefan and Schwoon, Stefan},
title = {Abstraction Refinement with {C}raig Interpolation
and Symbolic Pushdown Systems},
month = jun,
year = {2008},
volume = {5},
pages = {27-56},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EKS-jsat08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EKS-jsat08.pdf},
abstract = {Counterexample-guided abstraction refinement (CEGAR) has proven
to be a powerful method for software model-checking. In this
paper, we investigate this concept in the context of sequential
(possibly recursive) programs whose statements are given as
BDDs. We examine how Craig interpolants can be computed
efficiently in this case and propose a new, special type of
interpolants. Moreover, we show how to treat multiple
counterexamples in one refinement cycle. We have implemented
this approach within the model-checker Moped and report on
experiments.}
}
@inproceedings{SS-wmbs08,
address = {Patras, Greece},
month = jul,
year = 2008,
noseries = {},
acronym = {{MBS}'08},
booktitle = {{P}roceedings of the {ECAI}'08 {W}orkshop on {M}odel-{B}ased {S}ystems
({MBS}'08)},
author = {Martin Sachenbacher and Stefan Schwoon},
title = {Model-based Test Generation using Quantified {CSP}s: A~Map},
pages = {37-41}
}
@inproceedings{KSSK-fossacs09,
address = {York, UK},
month = mar,
year = 2009,
volume = 5504,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {de Alfaro, Luca},
acronym = {{FoSSaCS}'09},
booktitle = {{P}roceedings of the 12th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'09)},
author = {K{\"u}hnrich, Morten and Schwoon, Stefan
and Srba, Ji{\v{r}}{\'\i} and Kiefer, Stefan},
title = {Interprocedural Dataflow Analysis
over Weight Domains with Infinite Descending Chains},
pages = {440-455},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KSSK-fossacs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KSSK-fossacs09.pdf},
doi = {10.1007/978-3-642-00596-1_31},
abstract = {We study generalized fixed-point equations over idempotent
semirings and provide an efficient algorithm for the detection whether a
sequence of Kleene's iterations stabilizes after a finite number of steps.
Previously known approaches considered only bounded semirings where there
are no infinite descending chains. The main novelty of our work is that we
deal with semirings without the boundedness restriction. Our study is
motivated by several applications from interprocedural dataflow analysis.
We demonstrate how the reachability problem for weighted pushdown automata
can be reduced to solving equations in the framework mentioned above and
we describe a few applications to demonstrate its usability. }
}
@inproceedings{GS-memics09,
address = {Znojmo, Czech Republic},
month = nov,
year = 2009,
editor = {Hlin{\v e}n{\'y}, Petr and Maty{\'a}{\v s}, V{\'a}clav and Vojnar,
Tom{\'a}{\v{s}}},
acronym = {{MEMICS}'09},
booktitle = {{P}roceedings of the 5th {A}nnual {D}octoral {W}orkshop on {M}athematical
and {E}ngineering {M}ethods in {C}omputer {S}cience
({MEMICS}'09)},
author = {Gaiser, Andreas and Schwoon, Stefan},
title = {Comparison of algorithms for checking emptiness on B{\"u}chi automata},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GS-memics09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GS-memics09.pdf},
abstract = {We re-investigate the problem of LTL model-checking for
finite-state systems. Typical solutions, like in Spin, work on the fly,
reducing the problem to B{\"u}chi emptiness. This can be done in linear
time, and a variety of algorithms with this property exist. Nonetheless,
subtle design decisions can make a great difference to their actual
performance in practice, especially when used on-the-fly. We~compare a
number of algorithms experimentally on a large benchmark suite, measure
their actual run-time performance, and propose improvements. Compared with
the algorithm implemented in Spin, our best algorithm is faster by about
\(33\%\) on average. We therefore recommend that, for on-the-fly
explicit-state model checking, nested DFS should be replaced by better
solutions. }
}
@inproceedings{SR-dcfs11,
address = {Limburg, Germany},
month = jul,
year = 2011,
volume = {6808},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Holzer, Markus and Kutrib, Martin and Pighizzini, Giovanni},
acronym = {{DCFS}'11},
booktitle = {{P}roceedings of the 13th {I}nternational {W}orkshop on
{D}escriptional {C}omplexity of {F}ormal {S}ystems ({DCFS}'11)},
author = {Schwoon, Stefan and Rodr{\'\i}guez, C{\'e}sar},
title = {Construction and {SAT}-based verification
of Contextual Unfoldings},
pages = {34-42},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SR-dcfs11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SR-dcfs11.pdf},
doi = {10.1007/978-3-642-22600-7_3},
nonote = {Invited paper},
abstract = {Unfoldings succinctly represent the set of reachable markings of
a Petri net. Here, we shall consider the case of contextual nets, which
extend Petri nets with read arcs, and which are more suitable to represent
the case of concurrent read access. We discuss the problem of
(efficiently) constructing unfoldings of such nets. On the basis of these
unfoldings, various verification problems can be encoded as satisfiability
problems in propositional logic.}
}
@inproceedings{HKS-gandalf11,
address = {Minori, Italy},
month = jun,
year = 2011,
volume = 54,
series = {Electronic Proceedings in Theoretical Computer Science},
editor = {D'Agostino, Giovanna and La{~}Torre, Salvatore},
acronym = {{GandALF}'11},
booktitle = {{P}roceedings of the 2nd {I}nternational {S}ymposium
on {G}ames, {A}utomata, {L}ogics, and {F}ormal {V}erification
({GandALF}'11)},
author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan},
title = {Computing the Reveals Relation in Occurrence Nets},
pages = {31-44},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-gandalf11.pdf},
doi = {10.4204/EPTCS.54.3},
abstract = {Petri net unfoldings are a useful tool to tackle state-space
explosion in verification and related tasks. Moreover, their structure
allows to access directly the relations of causal precedence, concurrency,
and conflict between events. Here, we explore the data structure further,
to determine the following relation: event~\(a\) is said to reveal
event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably
occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of
reveals facilitates in particular the analysis of partially observable
systems, in the context of diagnosis, testing, or verification; it can
also be used to generate more concise representations of behaviours via
abstractions. The reveals relation was previously introduced in the
context of fault diagnosis, where it was shown that the reveals relation
was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe
Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide
whether or not \(a\) reveals~\(b\). In this paper, we first considerably
improve the bound on~\(|P|\). We then show that there exists an efficient
algorithm for computing the relation on a given prefix. We have
implemented the algorithm and report on experiments.}
}
@inproceedings{bbcks-icgt10,
address = {Enschede, The Netherlands},
month = sep # {-} # oct,
year = 2010,
volume = 6372,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Ehrig, Hartmut and Rensink, Arend
and Rozenberg, Grzegorz and Sch{\"u}rr, Andy},
acronym = {{ICGT}'10},
booktitle = {{P}roceedings of the 5th {I}nternational {C}onference on {G}raph
{T}ransformations ({ICGT}'10)},
author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea
and K{\"o}nig, Barbara and Schwoon, Stefan},
title = {On the Computation of {M}c{M}illan's Prefix for Contextual Nets
and Graph Grammars},
pages = {91-106},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbcks-icgt10.pdf},
doi = {10.1007/978-3-642-15928-2_7},
abstract = {In recent years, a research thread focused on the use of the
unfolding semantics for verification purposes. This started with a paper
by McMillan, which devises an algorithm for constructing a finite complete
prefix of the unfolding of a safe Petri net, providing a compact
representation of the reachability graph. The extension to contextual nets
and graph transformation systems is far from being trivial because events
can have multiple causal histories. Recently, we proposed an abstract
algorithm that generalizes McMillan's construction to bounded contextual
nets without resorting to an encoding into plain P\slash T nets. Here, we
provide a more explicit construction that renders the algorithm effective.
To allow for an inductive definition of concurrency, missing in the
original proposal and essential for an efficient unfolding procedure, the
key intuition is to associate histories not only with events, but also
with places. Additionally, we outline how the proposed algorithm can be
extended to graph transformation systems, for which previous algorithms
based on the encoding of read arcs would not be applicable.}
}
@inproceedings{RSB-concur11,
address = {Aachen, Germany},
month = sep,
year = 2011,
volume = 6901,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Katoen, Joost-Pieter and K{\"o}nig, Barbara},
acronym = {{CONCUR}'11},
booktitle = {{P}roceedings of the 22nd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'11)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Baldan, Paolo},
title = {Efficient contextual unfolding},
pages = {342-357},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RSB-concur11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RSB-concur11.pdf},
doi = {10.1007/978-3-642-23217-6_23},
abstract = {A~contextual net is a Petri net extended with read arcs, which
allow transitions to check for tokens without consuming them. Contextual
nets allow for better modelling of concurrent read access than Petri nets,
and their unfoldings can be exponentially more compact than those of a
corresponding Petri net. A~constructive but abstract procedure for
generating those unfoldings was proposed in earlier work; however, no
concrete implementation existed. Here, we~close this gap providing two
concrete methods for computing contextual unfoldings, with a view to
efficiency. We report on experiments carried out on a number of
benchmarks. These show that not only are contextual unfoldings more
compact than Petri net unfoldings, but they can be computed with the same
or better efficiency, in~particular with respect to the place-replication
encoding of contextual nets into Petri nets.}
}
@misc{cunf-v35,
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Cunf},
year = {2011},
month = feb,
number = {v35},
url = {http://www.lsv.ens-cachan.fr/Software/cunf/},
abstract = {The Cunf tool is a (contextual) Petri net unfolder implementing
the unfolding algorithm presented by Paolo Baldan et al. in 2008}
}
@article{bbckrs-tcs12,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Baldan, Paolo and Bruni, Alessandro and Corradini, Andrea
and K{\"o}nig, Barbara and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Efficient unfolding of contextual {P}etri nets},
volume = 449,
number = 1,
year = 2012,
month = aug,
pages = {2-22},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bbckrs-tcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bbckrs-tcs12.pdf},
doi = {10.1016/j.tcs.2012.04.046},
abstract = {A contextual net is a Petri net extended with read arcs, which
allows transitions to check for tokens without consuming them. Contextual
nets allow for better modelling of concurrent read access than Petri nets,
and their unfoldings can be exponentially more compact than those of a
corresponding Petri net. A constructive but abstract procedure for
generating those unfoldings was proposed in previous work. However, it
remained unclear whether the approach was useful in practice and which data
structures and algorithms would be appropriate to implement it. Here, we
address this question. We provide two concrete methods for computing
contextual unfoldings, with a view to efficiency. We report on experiments
carried out on a number of benchmarks. These show that not only are
contextual unfoldings more compact than Petri net unfoldings, but they can
be computed with the same or better efficiency, in particular with respect
to alternative approaches based on encodings of contextual nets into Petri
nets.}
}
@inproceedings{RS-concur12,
address = {Newcastle, UK},
month = sep,
year = 2012,
volume = 7454,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Koutny, Maciej and Ulidowski, Irek},
acronym = {{CONCUR}'12},
booktitle = {{P}roceedings of the 23rd
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'12)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Verification of {P}etri Nets with Read Arcs},
pages = {471-485},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-concur12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-concur12.pdf},
doi = {10.1007/978-3-642-32940-1_33},
abstract = {Recent work studied the unfolding construction for contextual
nets, i.e. nets with read arcs. Such unfoldings are more concise and can
usually be constructed more efficiently than for Petri nets. However,
concrete verification algorithms exploiting these advantages were lacking
so far. We address this question and propose SAT-based verification
algorithms for deadlock and reachability of contextual nets. Moreover, we
study optimizations of the SAT encoding and report on experiments.}
}
@phdthesis{schwoon-HDR13,
author = {Schwoon, Stefan},
title = {Efficient verification of sequential and concurrent systems},
year = 2013,
month = dec,
type = {M{\'e}moire d'habilitation},
school = {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-schwoon13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/hdr-schwoon13.pdf}
}
@inproceedings{HHMS-fsttcs13,
address = {Guwahati, India},
month = dec,
year = 2013,
volume = {24},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Seth, Anil and Vishnoi, Nisheeth},
acronym = {{FSTTCS}'13},
booktitle = {{P}roceedings of the 33rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'13)},
author = {Haar, Stefan and Haddad, Serge and Melliti, Tarek and Schwoon,
Stefan},
title = {Optimal Constructions for Active Diagnosis},
pages = {527-539},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS13-fsttcs.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2013.527},
abstract = {The task of diagnosis consists in detecting, without ambiguity,
occurrence of faults in a partially observed system. Depending on the
degree of observability, a discrete event system may be diagnosable or
not. Active diagnosis aims at controlling the system in order to make it
diagnosable. Solutions have already been proposed for the active diagnosis
problem, but their complexity remains to be improved. We solve here the
active diagnosability decision problem and the active diagnoser synthesis
problem, proving that (1)~our procedures are optimal w.r.t. to
computational complexity, and (2)~the memory required for the active
diagnoser produced by the synthesis is minimal. Furthermore, focusing on
the minimal delay before detection, we establish that the memory required
for any active diagnoser achieving this delay may be highly greater than
the previous one. So we refine our construction to build with the same
complexity and memory requirement an active diagnoser that realizes a
delay bounded by twice the minimal delay.}
}
@inproceedings{EJS-fsttcs13,
address = {Guwahati, India},
month = dec,
year = 2013,
volume = {24},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Seth, Anil and Vishnoi, Nisheeth},
acronym = {{FSTTCS}'13},
booktitle = {{P}roceedings of the 33rd {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'13)},
author = {Esparza, Javier and Jezequel, Lo{\"\i}g and Schwoon, Stefan},
title = {Computation of summaries using net unfoldings},
pages = {225-236},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/EJS-fsttcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/EJS-fsttcs13.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2013.225},
abstract = {We study the following summarization problem: given a parallel
composition \(A = A_1\Vert\cdots\Vert A_n\) of labelled transition systems
communicating with the environment through a distinguished component
\(A_i\), efficiently compute a summary~\(S_i\) such that \(E\Vert A\) and
\(E\Vert S_i\) are trace-equivalent for every environment~\(E\). While \(S_i\)
can be computed using elementary automata theory, the resulting algorithm
suffers from the state-explosion problem. We present a new, simple but
subtle algorithm based on net unfoldings, a partial-order semantics, give
some experimental results using an implementation on top of Mole, and show
that our algorithm can handle divergences and compute weighted summaries
with minor modifications.}
}
@inproceedings{RS-fsfma13,
address = {Singapore},
month = jul,
year = 2013,
volume = 31,
series = {Open Access Series in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Choppy, {\relax Ch}ristine and Sun, Jun},
acronym = {{FSFMA}'13},
booktitle = {{P}roceedings of the 1st {F}rench-{S}ingaporean {W}orkshop
on {F}ormal {M}ethods and {A}pplications ({FSFMA}'13)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {An Improved Construction of {P}etri Net Unfoldings},
pages = {47-52},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-fsfma13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-fsfma13.pdf},
doi = {10.4230/OASIcs.FSFMA.2013.47},
abstract = {Petri nets are a well-known model language for concurrent
systems. The unfolding of a Petri net is an acyclic net bisimilar to the
original one. Because it is acyclic, it admits simpler decision problems
though it is in general larger than the net. In this paper, we revisit the
problem of efficiently constructing an unfolding. We propose a new method
that avoids computing the concurrency relation and therefore uses less
memory than some other methods but still represents a good time-space
tradeoff. We implemented the approach and report on experiments.}
}
@inproceedings{RS-atva13,
address = {Hanoi, Vietnam},
month = oct,
year = {2013},
volume = {8172},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Dang{-}Van, Hung and Ogawa, Mizuhito},
acronym = {{ATVA}'13},
booktitle = {{P}roceedings of the 11th {I}nternational
{S}ymposium on {A}utomated {T}echnology
for {V}erification and {A}nalysis
({ATVA}'13)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Cunf: A~Tool for Unfolding and Verifying Petri Nets with Read
Arcs},
pages = {492-495},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-atva13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RS-atva13.pdf},
doi = {10.1007/978-3-319-02444-8_42},
abstract = {Cunf is a tool for building and analyzing unfoldings of Petri
nets with read arcs. An unfolding represents the behaviour of a net by a
partial order, effectively coping with the state-explosion problem
stemming from the interleaving of concurrent actions. C-net unfoldings can
be up to exponentially smaller than Petri net unfoldings, and recent work
proposed algorithms for their construction and verification. Cunf is the
first implementation of these techniques, it has been carefully engineered
and optimized to ensure that the theoretical gains are put into
practice.}
}
@inproceedings{HRS-acsd13,
address = {Barcelona, Spain},
month = jul,
year = 2013,
publisher = {{IEEE} Computer Society Press},
editor = {Pietkiewicz{-}Koutny, Marta and Lazarescu, Mihai Teodor},
acronym = {{ACSD}'13},
booktitle = {{P}roceedings of the 13th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'13)},
author = {Haar, Stefan and Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan},
title = {Reveal Your Faults: It's Only Fair!},
pages = {120-129},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HRS-acsd13.pdf},
doi = {10.1109/ACSD.2013.15},
abstract = {We present a methodology for fault diagnosis in
concurrent, partially observable systems with additional fairness
constraints. In this weak diagnosis, one asks whether a concurrent
chronicle of observed events allows to determine that a
non-observable fault will inevitably occur, sooner or later, on
any maximal system run compatible with the observation. The
approach builds on strengths and techniques of unfoldings of safe
Petri nets, striving to compute a compact prefix of the unfolding
that carries sufficient information for the diagnosis
algorithm. Our work extends and generalizes the unfolding-based
diagnosis approaches by Benveniste \textit{et~al.} as well as
Esparza and Kern. Both of these focused mostly on the use of
sequential observations, in particular did not exploit the
capacity of unfoldings to reveal inevitable occurrences of
concurrent or future events studied by Balaguer
\textit{et~al.}. Our diagnosis method captures such indirect,
revealed dependencies. We~develop theoretical foundations and an
algorithmic solution to the diagnosis problem, and present a SAT
solving method for practical diagnosis with our approach.}
}
@article{HKS-tcs13,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Haar, Stefan and Kern, Christian and Schwoon, Stefan},
title = {Computing the Reveals Relation in Occurrence Nets},
year = 2013,
month = jul,
volume = 493,
pages = {66-79},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HKS-tcs13.pdf},
doi = {10.1016/j.tcs.2013.04.028},
abstract = {Petri net unfoldings are a useful tool to tackle state-space
explosion in verification and related tasks. Moreover, their structure
allows to access directly the relations of causal precedence, concurrency,
and conflict between events. Here, we explore the data structure further,
to determine the following relation: event~\(a\) is said to reveal
event~\(b\) iff the occurrence of~\(a\) implies that~\(b\) inevitably
occurs, too, be it before, after, or concurrently with~\(a\). Knowledge of
reveals facilitates in particular the analysis of partially observable
systems, in the context of diagnosis, testing, or verification; it can
also be used to generate more concise representations of behaviours via
abstractions. The reveals relation was previously introduced in the
context of fault diagnosis, where it was shown that the reveals relation
was decidable: for a given pair~\(a,b\) in the unfolding~\(U\) of a safe
Petri net~\(N\), a finite prefix~\(P\) of~\(U\) is sufficient to decide
whether or not \(a\) reveals~\(b\). In this paper, we first considerably
improve the bound on~\(|P|\). We then show that there exists an efficient
algorithm for computing the relation on a given prefix. We have
implemented the algorithm and report on experiments.}
}
@inproceedings{RSK-pn13,
address = {Milano, Italy},
month = jun,
year = 2013,
volume = {7927},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Colom, Jos{\'e}-Manuel and Desel, J{\"o}rg},
acronym = {{PETRI~NETS}'13},
booktitle = {{P}roceedings of the 34th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'13)},
author = {Rodr{\'\i}guez, C{\'e}sar and Schwoon, Stefan and Khomenko,
Victor},
title = {Contextual Merged Processes},
pages = {29-48},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RSK-atpn13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/RSK-atpn13.pdf},
doi = {10.1007/978-3-642-38697-8_3},
abstract = {We integrate two compact data structures for
representing state spaces of Petri nets: merged processes and
contextual prefixes. The resulting data structure, called
contextual merged processes (CMP), combines the advantages of the
original ones and copes with several important sources of state
space explosion: concurrency, sequences of choices, and concurrent
read accesses to shared resources. In particular, we demonstrate
on a number of benchmarks that CMPs are more compact than either
of the original data structures. Moreover, we sketch a polynomial
(in the CMP size) encoding into SAT of the model-checking problem
for reachability properties.}
}
@inproceedings{CMS-fsttcs14,
address = {New~Dehli, India},
month = dec,
year = 2014,
volume = {29},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Raman, Venkatesh and Suresh, S.~P.},
acronym = {{FSTTCS}'14},
booktitle = {{P}roceedings of the 34th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'14)},
author = {Chadha, Rohit and Mathur, Umang and Schwoon, Stefan},
title = {Computing Information Flow Using Symbolic Model-Checking},
pages = {505-516},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CMS-fsttcs14.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2014.505},
abstract = {Several measures have been proposed in literature for
quantifying the information leaked by the public outputs of a program with
secret inputs. We consider the problem of computing information leaked by
a deterministic or probabilistic program when the measure of information
is based on (a)~min-entropy and (b)~Shannon entropy. The key challenge in
computing these measures is that we need the total number of possible
outputs and, for each possible output, the number of inputs that lead to
it. A direct computation of these quantities is infeasible because of the
state-explosion problem. We therefore propose symbolic algorithms based on
binary decision diagrams (BDDs). The advantage of our approach is that
these symbolic algorithms can be easily implemented in any BDD-based
model-checking tool that checks for reachability in deterministic
non-recursive programs by computing program summaries. We demonstrate the
validity of our approach by implementing these algorithms in a tool
Moped-QLeak, which is built upon Moped, a model checker for Boolean
programs. Finally, we show how this symbolic approach extends to
probabilistic programs.}
}
@inproceedings{CHJPS-cmsb14,
address = {Manchester, UK},
month = nov,
year = 2014,
volume = {8859},
series = {Lecture Notes in Bioinformatics},
publisher = {Springer-Verlag},
editor = {Mendes, Pedro},
acronym = {{CMSB}'14},
booktitle = {{P}roceedings of the 12th
{C}onference on
{C}omputational {M}ethods in {S}ystem {B}iology
({CMSB}'14)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Jezequel,
Lo{\"\i}g and Paulev{\'e}, Lo{\"\i}c and Schwoon, Stefan},
title = {Characterization of Reachable Attractors Using {P}etri Net
Unfoldings},
pages = {129-142},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHJPS-cmsb14.pdf},
doi = {10.1007/978-3-319-12982-2_10},
abstract = {Attractors of network dynamics represent the long-term
behaviours of the modelled system. Their characterization is therefore
crucial for understanding the response and differentiation capabilities of
a dynamical system. In the scope of qualitative models of interaction
networks, the computation of attractors reachable from a given state of
the network faces combinatorial issues due to the state space explosion.
In this paper, we present a new algorithm that exploits the concurrency
between transitions of parallel acting components in order to reduce the
search space. The algorithm relies on Petri net unfoldings that can be
used to compute a compact representation of the dynamics. We illustrate
the applicability of the algorithm with Petri net models of cell
signalling and regulation networks, Boolean and multi-valued. The proposed
approach aims at being complementary to existing methods for deriving the
attractors of Boolean models, while being generic since they apply to any
safe Petri net.}
}
@inproceedings{GHKS-acsd14,
address = {Tunis, Tunisia},
month = jun,
year = 2014,
publisher = {{IEEE} Computer Society Press},
acronym = {{ACSD}'14},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {A}pplication of {C}oncurrency
to {S}ystem {D}esign
({ACSD}'14)},
author = {Germanos, Vasileios and Haar, Stefan
and Khomenko, Victor and Schwoon, Stefan},
title = {Diagnosability under Weak Fairness},
pages = {132-141},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-acsd14.pdf},
doi = {10.1109/ACSD.2014.9},
abstract = {In partially observed Petri nets, diagnosis is the
task of detecting whether or not the given sequence of
observed labels indicates that some unobservable fault
has occurred. Diagnosability is an associated property of
the Petri net, stating that in any possible execution an
occurrence of a fault can eventually be diagnosed.\par In this
paper we consider diagnosability under the weak fairness (WF)
assumption, which intuitively states that no transition from
a given set can stay enabled forever---it~must eventually
either fire or be disabled. We show that a previous approach
to WF-diagnosability in the literature has a major flaw, and
present a corrected notion. Moreover, we present an efficient
method for verifying WF-diagnosability based on a reduction
to LTL-X model checking. An important advantage of this
method is that the LTL-X formula is fixed---in~particular,
the WF assumption does not have to be expressed as a part of
it (which would make the formula length proportional to the
size of the specification), but rather the ability of existing
model checkers to handle weak fairness directly is exploited.}
}
@article{GHKS-tecs15,
publisher = {ACM Press},
journal = {ACM Transactions in Embedded Computing Systems},
author = {Germanos, Vasileios and Haar, Stefan
and Khomenko, Victor and Schwoon, Stefan},
title = {Diagnosability under Weak Fairness},
volume = 14,
number = {4:69},
nopages = {},
month = dec,
year = 2015,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GHKS-tecs15.pdf},
doi = {10.1145/2832910},
abstract = {In partially observed Petri nets, diagnosis is the task of
detecting whether or not the given sequence of observed labels indicates
that some unobservable fault has occurred. Diagnosability is an associated
property of the Petri net, stating that in any possible execution an
occurrence of a fault can eventually be diagnosed.\par
In this paper we consider diagnosability under the weak fairness (WF)
assumption, which intuitively states that no transition from a given set
can stay enabled forever---it~must eventually either fire or be disabled.
We show that a previous approach to WF-diagnosability in the literature
has a major flaw, and present a corrected notion. Moreover, we present an
efficient method for verifying WF-diagnosability based on a reduction to
LTL-X model checking. An~important advantage of this method is that the
LTL-X formula is fixed---in~particular, the WF assumption does not have to
be expressed as a part of it (which would make the formula length
proportional to the size of the specification), but rather the ability of
existing model checkers to handle weak fairness directly is exploited.}
}
@inproceedings{BHHHS-cdc15,
address = {Osaka, Japan},
month = dec,
year = 2015,
publisher = {{IEEE} Control System Society},
noeditor = {},
acronym = {{CDC}'15},
booktitle = {{P}roceedings of the 54th {IEEE} {C}onference on
{D}ecision and {C}ontrol ({CDC}'15)},
author = {B{\"o}hm, Stanislav and Haar, Stefan and Haddad, Serge and
Hofman, Piotr and Schwoon, Stefan},
title = {Active Diagnosis with Observable Quiescence},
pages = {1663-1668},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BHHHS-cdc15.pdf},
doi = {10.1109/CDC.2015.7402449},
abstract = {Active diagnosis of a discrete-event system consists in
controlling the system such that faults can be detected. Here we extend
the framework of active diagnosis by introducing modalities for actions
and states and a new capability for the controller, namely observing that
the system is quiescent. We design a game-based construction for both the
decision and the synthesis problems that is computationally optimal.
Furthermore we prove that the size and the delay provided by the active
diagnoser (when it exists) are almost optimal.}
}
@inproceedings{CHKS-pn15,
address = {Brussels, Belgium},
month = jun,
year = 2015,
volume = {9115},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Devillers, Raymond and Valmari, Antti},
acronym = {{PETRI~NETS}'15},
booktitle = {{P}roceedings of the 36th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'15)},
author = {Chatain, {\relax Th}omas and Haar, Stefan and Koutny,
Maciej and Schwoon, Stefan},
title = {Non-Atomic Transition Firing in Contextual Nets},
pages = {117-136},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CHKS-pn15.pdf},
doi = {10.1007/978-3-319-19488-2_6},
abstract = {The firing rule for Petri nets assumes instantaneous and
simultaneous consumption and creation of tokens. In the context of
ordinary Petri nets, this poses no particular problem because of the
system's asynchronicity, even if token creation occurs later than token
consumption in the firing. With read arcs, the situation changes, and
several different choices of semantics are possible. The step semantics
introduced by Janicki and Koutny can be seen as imposing a two-phase
firing scheme: first, the presence of the required tokens is checked, then
consumption and production of tokens happens. Pursuing this approach
further, we develop a more general framework based on explicitly splitting
the phases of firing, allowing to synthesize coherent steps. This turns
out to define a more general non-atomic semantics, which has important
potential for safety as it allows to detect errors that were missed by the
previous semantics. Then we study the characterization of partial-order
processes feasible under one or the other semantics.}
}
@article{HHMS-jcss16,
publisher = {Elsevier Science Publishers},
journal = {Journal of Computer and System Sciences},
author = {Stefan Haar and
Serge Haddad and
Tarek Melliti and
Stefan Schwoon},
title = {Optimal constructions for active diagnosis},
pages = {101-120},
volume = {83},
number = {1},
year = {2017},
doi = {10.1016/j.jcss.2016.04.007},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HHMS-jcss16.pdf},
abstract = {Diagnosis is the task of detecting fault occurrences in a partially observed sys- tem. Depending on the possible observations, a discrete-event system may be diagnosable or not. Active diagnosis aims at controlling the system to render it diagnosable. Past research has proposed solutions for this problem, but their complexity remains to be improved. Here, we solve the decision and synthesis problems for active diagnosability, proving that (1) our procedures are optimal with respect to computational complexity, and (2) the memory required for our diagnoser is minimal. We then study the delay between a fault occurrence and its detection by the diagnoser. We construct a memory-optimal diagnoser whose delay is at most twice the minimal delay, whereas the memory required to achieve optimal delay may be highly greater. We also provide a solution for parametrized active diagnosis, where we automatically construct the most permissive controller respecting a given delay.}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{APS-tap15,
address = {L'Aquila, Italy},
month = jul,
year = 2015,
volume = 9154,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = { Blanchette, Jasmin Christian and Kosmatov, Nikolai},
acronym = {{TAP}'15},
booktitle = {{P}roceedings of the 9th {I}nternational {C}onference
on {T}ests and {P}roofs ({TAP}'15)},
author = {Athanasiou, Konstantinos and Ponce{ }de{~}Le{\'o}n, Hern\'an
and Schwoon, Stefan},
title = {Test Case Generation for Concurrent Systems
Using Event Structures},
pages = {19-37},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/APS-tap15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/APS-tap15.pdf},
doi = {10.1007/978-3-319-21215-9_2},
abstract = {This paper deals with the test-case generation problem for
concurrent systems that are specified by true-concurrency models such as
Petri nets. We show that using true-concurrency models reduces both the
size and the number of test cases needed for achieving certain coverage
criteria. We present a test-case generation algorithm based on Petri net
unfoldings and a SAT encoding for solving controllability problems in test
cases. Finally, we evaluate our algorithm against traditional test-case
generation methods under interleaving semantics.}
}
@inproceedings{BHSS-pn17,
address = {Zaragoza, Spain},
month = jun,
volume = {10258},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van der Aalst, Wifred and Best, Eike},
acronym = {{PETRI~NETS}'17},
booktitle = {{P}roceedings of the 38th
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'17)},
author = {B{\'e}rard, B{\'e}atrice and Haar, Stefan and
Schmitz, Sylvain and Schwoon, Stefan},
title = {The Complexity of Diagnosability and Opacity
Verification for {P}etri Nets},
pages = {200-220},
year = {2017},
doi = {10.1007/978-3-319-57861-3_13},
url = {https://hal.inria.fr/hal-01484476},
abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@inproceedings{JMS-wodes18,
address = {Sorrento Coast, Italy},
month = may # {-} # jun,
year = 2018,
volume = {51(7)},
series = {IFAC-PapersOnLine},
publisher = {Elsevier Science Publishers},
editor = {Chris Hadjicostis and Jan Komenda},
acronym = {{WODES}'18},
booktitle = {{P}roceedings of the 14th {W}orkshop on {D}iscrete {E}vent {S}ystems
({WODES}'18)},
author = {Lo{\"i}g Jezequel and Agnes Madalinski and Stefan Schwoon},
title = {{Distributed computation of vector clocks in Petri nets unfolding for test selection}},
pages = {106-111},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JMS-wodes18.pdf},
abstract = {It has been shown that annotating Petri net unfoldings with time stamps allows for
building distributed testers for distributed systems. However, the construction of the annotated
unfolding of a distributed system currently remains a centralized task. In this paper we extend
a distributed unfolding technique in order to annotate the resulting unfolding with time stamps.
This allows for distributed construction of distributed testers for distributed systems.}
}
@article{BHSS-fi18,
publisher = {{IOS} Press},
journal = {Fundamenta Informaticae},
author = {B{\'e}atrice B{\'e}rard and Stefan Haar and Sylvain Schmitz and Stefan Schwoon},
title = {{The Complexity of Diagnosability and Opacity Verification for Petri Nets}},
volume = 161,
number = 4,
year = 2018,
pages = {317-349},
doi = {10.3233/FI-2018-1706},
url = {https://hal.inria.fr/hal-01852119},
abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues.
\par
We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions.
\par
Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@article{JMS-deds20,
publisher = {Springer},
journal = {Discrete Event Dynamic Systems: Theory and Applications},
author = {Lo{\"i}g Jezequel and Agnes Madalinski and Stefan Schwoon},
title = {{Distributed computation of vector clocks in Petri net unfoldings for test selection}},
volume = {30},
number = {3},
pages = {441-464},
year = {2020}
}
@inproceedings{HPS-cmsb20,
address = {held online},
month = sep,
volume = {12314},
series = {Lecture Notes in Bioinformatics},
publisher = {Springer-Verlag},
editor = {Alessandro Abate and Tatjana Petrov and Verena Wolf},
acronym = {{CMSB}'20},
booktitle = {{P}roceedings of the 18th
{C}onference on
{C}omputational {M}ethods in {S}ystem {B}iology
({CMSB}'20)},
author = {Stefan Haar and Lo{\"i}c Paulev{\'e} and Stefan Schwoon},
title = {{Drawing the Line: Basin Boundaries in Safe Petri Nets}},
pages = {321-336},
year = {2020},
doi = {10.1007/978-3-030-60327-4\_17}
}
@inproceedings{HHSY-fsttcs20,
address = {Goa, India},
month = dec,
volume = {182},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Nitin Saxena and Sunil Simon},
acronym = {{FSTTCS}'20},
booktitle = {{P}roceedings of the 40th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'20)},
author = {Stefan Haar and Serge Haddad and Stefan Schwoon and Lina Ye},
title = {Active Prediction for Discrete Event Systems},
pages = {48:1--48:16},
year = {2020},
doi = {https://doi.org/10.4230/LIPIcs.FSTTCS.2020.48},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2020/13289/pdf/LIPIcs-FSTTCS-2020-48.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13289}
}
This file was generated by bibtex2html 1.98.