Volume

OASIcs, Volume 13

Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)

Thumbnail PDF

Event

MEMICS 2009, November 13-15, 2009, Znojmo, Czech Republic

Editors

Petr Hlinený
Václav Matyáš
Tomáš Vojnar

Publication Details

  • published at: 2009-12-15
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
  • ISBN: 978-3-939897-15-6
  • DBLP: db/conf/memics/memics2009

Access Numbers

Documents

No documents found matching your filter selection.
Document
Complete Volume
DOI: 10.4230/OASIcs.MEMICS.2009
OASIcs, Volume 13, MEMICS'09, Complete Volume

Authors: Petr Hlinený, Václav Matyáš, and Tomáš Vojnar

Abstract
OASIcs, Volume 13, MEMICS'09, Complete Volume
Cite as

Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Proceedings{hlineny_et_al:OASIcs.MEMICS.2009,
  title =	{{OASIcs, Volume 13, MEMICS'09, Complete Volume}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.MEMICS.2009},
  URN =		{urn:nbn:de:0030-drops-35756},
  doi =		{10.4230/OASIcs.MEMICS.2009},
  annote =	{Keywords: Mathematics of Computing, Physical Sciences and Engineering}
}
Document
Front Matter
DOI: 10.4230/DROPS.MEMICS.2009.2342
Preface -- Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)

Authors: Petr Hlinený, Václav Matyáš, and Tomáš Vojnar

Abstract
The 2009 edition of the International Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) is the fifth in a~row of three-day workshops organized in South Moravia by Faculty of Information Technology of Brno University of Technology and Faculty of Informatics of Masaryk University. MEMICS'09 was held in Znojmo, Czech Republic, on November 13--15, 2009.
Cite as

Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. i-vi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{hlineny_et_al:OASIcs:2009:DROPS.MEMICS.2009.2342,
  author =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  title =	{{Preface -- Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{i--vi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2342},
  URN =		{urn:nbn:de:0030-drops-23425},
  doi =		{10.4230/DROPS.MEMICS.2009.2342},
  annote =	{Keywords: MEMICS 2009}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2355
A Privacy-Aware Protocol for Sociometric Questionnaires

Authors: Marián Novotný

Abstract
In the paper we design a protocol for sociometric questionnaires, which serves the privacy of responders. We propose a representation of a sociogram by a weighted digraph and interpret individual and collective phenomena of sociometry in terms of graph theory. We discuss security requirements for a privacy-aware protocol for sociometric questionnaires. In the scheme we use additively homomorphic public key cryptosystem, which allows single multiplication. We present the threshold version of the public key system and define individual phases of the scheme. The proposed protocol ensures desired security requirements and can compute sociometric indices without revealing private information about choices of responders.
Cite as

Marián Novotný. A Privacy-Aware Protocol for Sociometric Questionnaires. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{novotny:OASIcs:2009:DROPS.MEMICS.2009.2355,
  author =	{Novotn\'{y}, Mari\'{a}n},
  title =	{{A Privacy-Aware Protocol for Sociometric Questionnaires}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{1--9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2355},
  URN =		{urn:nbn:de:0030-drops-23551},
  doi =		{10.4230/DROPS.MEMICS.2009.2355},
  annote =	{Keywords: Sociometry, sociogram, privacy, homomorphic encryption, security protocols}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2345
A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

Authors: Kim G. Larsen, Uli Fahrenberg, and Claus Thrane

Abstract
We extend the usual notion of Kripke Structures with a weighted transition relation, and generalize the usual Boolean satisfaction relation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax, and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation.
Cite as

Kim G. Larsen, Uli Fahrenberg, and Claus Thrane. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 10-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:OASIcs:2009:DROPS.MEMICS.2009.2345,
  author =	{Larsen, Kim G. and Fahrenberg, Uli and Thrane, Claus},
  title =	{{A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{10--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2345},
  URN =		{urn:nbn:de:0030-drops-23454},
  doi =		{10.4230/DROPS.MEMICS.2009.2345},
  annote =	{Keywords: Quantitative analysis, Kripke structures, characteristic formulae, bisimulation distance, weighted CTL}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2349
Comparison of Algorithms for Checking Emptiness on Büchi Automata

Authors: Andreas Gaiser and Stefan Schwoon

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ü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.
Cite as

Andreas Gaiser and Stefan Schwoon. Comparison of Algorithms for Checking Emptiness on Büchi Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 18-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{gaiser_et_al:OASIcs:2009:DROPS.MEMICS.2009.2349,
  author =	{Gaiser, Andreas and Schwoon, Stefan},
  title =	{{Comparison of Algorithms for Checking Emptiness on B\"{u}chi Automata}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{18--26},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2349},
  URN =		{urn:nbn:de:0030-drops-23494},
  doi =		{10.4230/DROPS.MEMICS.2009.2349},
  annote =	{Keywords: LTL Model checking, Depth first search}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2351
Derivation in Scattered Context Grammar via Lazy Function Evaluation

Authors: Ota Jirák and Dušan Kolář

Abstract
This paper discusses scattered context grammars (SCG) and considers the application of scattered context grammar production rules. We use function that represents single derivation step over the given sentential form. Moreover, we define this function in such a way, so that it represents the delayed execution of scattered context grammar production rules using the same principles as a lazy evaluation in functional programming. Finally, we prove equivalence of the usual and the delayed execution of SCG production rules.
Cite as

Ota Jirák and Dušan Kolář. Derivation in Scattered Context Grammar via Lazy Function Evaluation. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 27-36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{jirak_et_al:OASIcs:2009:DROPS.MEMICS.2009.2351,
  author =	{Jir\'{a}k, Ota and Kol\'{a}\v{r}, Du\v{s}an},
  title =	{{Derivation in Scattered Context Grammar via Lazy Function Evaluation}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{27--36},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2351},
  URN =		{urn:nbn:de:0030-drops-23517},
  doi =		{10.4230/DROPS.MEMICS.2009.2351},
  annote =	{Keywords: SCG, delayed execution, derivation, lazy evaluation}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2353
Embedded Process Functional Language

Authors: Marek Bĕhálek and Petr Šaloun

Abstract
Embedded systems represent an important area of computer engineering. Demands on embedded applications are increasing. To address these issues, different agile methodologies are used in traditional desktop applications today. These agile methodologies often try to eliminate development risks in early design phases. Possible solution is to create a working model or a prototype of critical system parts. Then we can use this prototype in negotiation with customer and also to prove technological aspects of our solution. From this perspective functional languages are very attractive. They have excellent abstraction mechanism and they can be used as a tool producing a kind of executable design. In this paper we present our work on a domain specific functional language targeted to embedded systems Embedded process functional language. Created language works on a high level of abstraction and it uses other technologies (even other functional languages) created for embedded systems development on lower levels. It can be used like a modeling or a prototyping language in early development phases.
Cite as

Marek Bĕhálek and Petr Šaloun. Embedded Process Functional Language. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 37-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{behalek_et_al:OASIcs:2009:DROPS.MEMICS.2009.2353,
  author =	{B\u{e}h\'{a}lek, Marek and \v{S}aloun, Petr},
  title =	{{Embedded Process Functional Language}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{37--44},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2353},
  URN =		{urn:nbn:de:0030-drops-23535},
  doi =		{10.4230/DROPS.MEMICS.2009.2353},
  annote =	{Keywords: Embedded systems, model, high abstraction level, functional programming}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2343
Exact Quantum Query Algorithm for Error Detection Code Verification

Authors: Alina Vasilieva

Abstract
Quantum algorithms can be analyzed in a query model to compute Boolean functions. Function input is provided in a black box, and the aim is to compute the function value using as few queries to the black box as possible. A repetition code is an error detection scheme that repeats each bit of the original message r times. After a message with redundant bits is transmitted via a communication channel, it must be verified. If the received message consists of r-size blocks of equal bits, the conclusion is that there were no errors. The verification procedure can be interpreted as an application of a query algorithm, where input is a message to be checked. Classically, for N-bit message, values of all N variables must be queried. We demonstrate an exact quantum algorithm that uses only N/2 queries.
Cite as

Alina Vasilieva. Exact Quantum Query Algorithm for Error Detection Code Verification. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 45-52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{vasilieva:OASIcs:2009:DROPS.MEMICS.2009.2343,
  author =	{Vasilieva, Alina},
  title =	{{Exact Quantum Query Algorithm for Error Detection Code Verification}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{45--52},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2343},
  URN =		{urn:nbn:de:0030-drops-23434},
  doi =		{10.4230/DROPS.MEMICS.2009.2343},
  annote =	{Keywords: Quantum computing, quantum query algorithms, algorithm complexity, Boolean functions, algorithm design}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2348
Faster Algorithm for Mean-Payoff Games

Authors: Jakub Chaloupka and Luboš Brim

Abstract
We study some existing techniques for solving mean-payoff games (MPGs), improve them, and design a randomized algorithm for solving MPGs with currently the best expected complexity.
Cite as

Jakub Chaloupka and Luboš Brim. Faster Algorithm for Mean-Payoff Games. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 53-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{chaloupka_et_al:OASIcs:2009:DROPS.MEMICS.2009.2348,
  author =	{Chaloupka, Jakub and Brim, Lubo\v{s}},
  title =	{{Faster Algorithm for Mean-Payoff Games}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{53--61},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2348},
  URN =		{urn:nbn:de:0030-drops-23481},
  doi =		{10.4230/DROPS.MEMICS.2009.2348},
  annote =	{Keywords: Mean-payoff games, randomized algorithms, computational complexity}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2347
One size does not fit all - how to approach intrusion detection in wireless sensor networks

Authors: Andriy Stetsko and Václav Matyáš

Abstract
A wireless sensor network (WSN) is a highly distributed network of resource constrained and wireless devices called sensor nodes. In the work we consider intrusion detection systems as they are proper mechanisms to defend internal attacks on WSNs. A wide diversity of WSN applications on one side and limited resources on other side implies that "one-fit-all" intrusion detection system is not optimal. We present a conceptual proposal for a suite of tools that enable an automatic design of intrusion detection system that will be (near) optimal for a given network topology, capabilities of sensor nodes and anticipated attacks.
Cite as

Andriy Stetsko and Václav Matyáš. One size does not fit all - how to approach intrusion detection in wireless sensor networks. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 62-69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{stetsko_et_al:OASIcs:2009:DROPS.MEMICS.2009.2347,
  author =	{Stetsko, Andriy and Maty\'{a}\v{s}, V\'{a}clav},
  title =	{{One size does not fit all - how to approach intrusion detection in wireless sensor networks}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{62--69},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2347},
  URN =		{urn:nbn:de:0030-drops-23479},
  doi =		{10.4230/DROPS.MEMICS.2009.2347},
  annote =	{Keywords: Intrusion detection, wireless sensor networks}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2356
Rewriting Systems over Nested Data Words

Authors: Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu

Abstract
We propose a generic framework for reasoning about infinite state systems handling data like integers, booleans etc. and having complex control structures. We consider that configurations of such systems are represented by nested data words, i.e., words of ... words over a potentially infinite data domain. We define a logic called $\ndwl$ allowing to reason about nested data words, and we define rewriting systems called $\ndwrs$ over these nested structures. The rewriting systems are constrained by formulas in the logic specifying the rewriting positions as well as structure/data transformations. We define a fragment $\Sigma_2^*$ of $\ndwl$ with a decidable satisfiability problem. Moreover, we show that the transition relation defined by rewriting systems with $\Sigma_2^*$ constraints can be effectively defined in the same fragment. These results can be used in the automatization of verification problems such as inductive invariance checking and bounded reachability analysis. Our framework allows to reason about a wide range of concurrent systems including multithreaded programs (with procedure calls, thread creation, global/local variables over infinite data domains, locks, monitors, etc.), dynamic networks of timed systems, cache coherence/mutex/communication protocols, etc.
Cite as

Ahmed Bouajjani, Cezara Drăgoi, Yan Jurski, and Mihaela Sighireanu. Rewriting Systems over Nested Data Words. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 70-79, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:OASIcs:2009:DROPS.MEMICS.2009.2356,
  author =	{Bouajjani, Ahmed and Dr\u{a}goi, Cezara and Jurski, Yan and Sighireanu, Mihaela},
  title =	{{Rewriting Systems over Nested Data Words}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{70--79},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2356},
  URN =		{urn:nbn:de:0030-drops-23567},
  doi =		{10.4230/DROPS.MEMICS.2009.2356},
  annote =	{Keywords: Nested data words, rewriting systems, program verification, dynamic and parametrized systems, invariance checking}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2354
Space Effective Model Checking for Component-Interaction Automata

Authors: Nikola Beneš, Milan Křivánek, and Filip Štefaňák

Abstract
The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic. As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample set partial order reduction method within the component-interaction automata verification framework. Due to the state and action-based nature of both the modelling and specification formalisms, the implementation differs from traditional state-based approaches. After describing the implementation, we present some of the results obtained by employing the enhanced verification framework on a case study.
Cite as

Nikola Beneš, Milan Křivánek, and Filip Štefaňák. Space Effective Model Checking for Component-Interaction Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 80-87, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{benes_et_al:OASIcs:2009:DROPS.MEMICS.2009.2354,
  author =	{Bene\v{s}, Nikola and K\v{r}iv\'{a}nek, Milan and \v{S}tefa\v{n}\'{a}k, Filip},
  title =	{{Space Effective Model Checking for Component-Interaction Automata}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{80--87},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2354},
  URN =		{urn:nbn:de:0030-drops-23549},
  doi =		{10.4230/DROPS.MEMICS.2009.2354},
  annote =	{Keywords: Model checking, component-based systems, partial order reduction}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2350
The Parameterized Complexity of Oriented Colouring

Authors: Robert Ganian

Abstract
The oriented colouring problem is intuitive and related to undirected colouring, yet remains NP-hard even on digraph classes with bounded traditional directed width measures. Recently we have also proved that it remains NP-hard in otherwise severely restricted digraph classes. However, unlike most other problems on directed graphs, the oriented colouring problem is not directly transferable to undirected graphs. In the article we look at the parameterized complexity of computing the oriented colouring of digraphs with bounded undirected width parameters, whereas the parameters ``forget'' about the orientations of arcs and treat them as edges. Specifically, we provide new complexity results for computing oriented colouring on digraphs of bounded undirected rank-width and a new algorithm for this problem on digraphs of bounded undirected tree-width.
Cite as

Robert Ganian. The Parameterized Complexity of Oriented Colouring. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 88-95, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{ganian:OASIcs:2009:DROPS.MEMICS.2009.2350,
  author =	{Ganian, Robert},
  title =	{{The Parameterized Complexity of Oriented Colouring}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{88--95},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2350},
  URN =		{urn:nbn:de:0030-drops-23500},
  doi =		{10.4230/DROPS.MEMICS.2009.2350},
  annote =	{Keywords: Oriented colouring, tree-width, rank-width, parameterized algorithms, graphs}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2352
Towards Comparing the Robustness of Synchronous and Asynchronous Circuits by Fault Injection

Authors: Marcus Jeitler and Jakob Lechner

Abstract
As transient error rates are growing due to smaller feature sizes, designing reliable synchronous circuits becomes increasingly challenging. Asynchronous logic design constitutes a promising alternative with respect to robustness and stability. In particular, delay-insensitive asynchronous circuits provide interesting properties, like an inherent resilience to delay-faults.
Cite as

Marcus Jeitler and Jakob Lechner. Towards Comparing the Robustness of Synchronous and Asynchronous Circuits by Fault Injection. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 96-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{jeitler_et_al:OASIcs:2009:DROPS.MEMICS.2009.2352,
  author =	{Jeitler, Marcus and Lechner, Jakob},
  title =	{{Towards Comparing the Robustness of Synchronous and Asynchronous Circuits by Fault Injection}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{96--105},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2352},
  URN =		{urn:nbn:de:0030-drops-23529},
  doi =		{10.4230/DROPS.MEMICS.2009.2352},
  annote =	{Keywords: Four State Logic, Asynchronous Design, Fault Injection, Fault Tolerance}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2346
Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants

Authors: Lasse Jacobsen, Morten Jacobsen, and Mikael H. Møller

Abstract
Timed-Arc Petri Nets (TAPN) is a well studied extension of the classical Petri net model where tokens are decorated with real numbers that represent their age. Unlike reachability, which is known to be undecidable for TAPN, boundedness and coverability remain decidable. The model is supported by a recent tool called TAPAAL which, among others, further extends TAPN with invariants on places in order to model urgency. The decidability of boundedness and coverability for this extended model has not yet been considered. We present a reduction from two-counter Minsky machines to TAPN with invariants to show that both the boundedness and coverability problems are undecidable.
Cite as

Lasse Jacobsen, Morten Jacobsen, and Mikael H. Møller. Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 106-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{jacobsen_et_al:OASIcs:2009:DROPS.MEMICS.2009.2346,
  author =	{Jacobsen, Lasse and Jacobsen, Morten and M{\o}ller, Mikael H.},
  title =	{{Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{106--113},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2346},
  URN =		{urn:nbn:de:0030-drops-23461},
  doi =		{10.4230/DROPS.MEMICS.2009.2346},
  annote =	{Keywords: Timed-Arc Petri Nets, Undecidability, Coverability, Boundedness}
}
Document
DOI: 10.4230/DROPS.MEMICS.2009.2344
Weighted Dynamic Pushdown Networks

Authors: Alexander Wenner

Abstract
We develop a generic framework for the analysis of programs with recursive procedures and dynamic process creation. To this end we combine the approach of weighted pushdown systems (WPDS) with the model of dynamic pushdown networks (DPN). Weighted dynamic pushdown networks (WDPN) describe processes running in parallel. Each process may perform pushdown actions and spawn new processes. Transitions are labelled by weights to carry additional information. We derive a method to determine meet-over-all-paths values for the paths from a starting configuration to a regular set of configurations of a WDPN.
Cite as

Alexander Wenner. Weighted Dynamic Pushdown Networks. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 114-121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{wenner:OASIcs:2009:DROPS.MEMICS.2009.2344,
  author =	{Wenner, Alexander},
  title =	{{Weighted Dynamic Pushdown Networks}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{114--121},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2344},
  URN =		{urn:nbn:de:0030-drops-23440},
  doi =		{10.4230/DROPS.MEMICS.2009.2344},
  annote =	{Keywords: Program analysis, recursive procedures, dynamic process creation, dataflow analysis}
}

Filters

  • Authors
  • B
  • Bĕhálek, Marek
  • Beneš, Nikola
  • Bouajjani, Ahmed
  • Brim, Luboš
  • C
  • Chaloupka, Jakub
  • D
  • Drăgoi, Cezara
  • F
  • Fahrenberg, Uli
  • G
  • Gaiser, Andreas
  • Ganian, Robert
  • H
  • Hlinený, Petr
  • J
  • Jacobsen, Lasse
  • Jacobsen, Morten
  • Jeitler, Marcus
  • Jirák, Ota
  • Jurski, Yan
  • K
  • Kolář, Dušan
  • Křivánek, Milan
  • L
  • Larsen, Kim G.
  • Lechner, Jakob
  • M
  • Matyáš, Václav
  • Møller, Mikael H.
  • N
  • Novotný, Marián
  • S
  • Šaloun, Petr
  • Schwoon, Stefan
  • Sighireanu, Mihaela
  • Štefaňák, Filip
  • Stetsko, Andriy
  • T
  • Thrane, Claus
  • V
  • Vasilieva, Alina
  • Vojnar, Tomáš
  • W
  • Wenner, Alexander

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact