Technical Reports

A list with abstracts sorted by year - 2011

Employing Subsequence Matching in Audio Data Processing

by Petr Volny, David Novák, Pavel Zezula, September 2011, 29 pages.

FIMU-RS-2011-04. Available as Postscript, PDF.

Abstract:

We overview current problems of audio retrieval and time-series subsequence matching. We discuss the usage of subsequence matching approaches in audio data processing, especially in automatic speech recognition (ASR) area and we aim at improving performance of the retrieval process. To overcome the problems known from the time-series area like the occurrence of implementation bias and data bias we present a Subsequence Matching Framework as a tool for fast prototyping, building, and testing similarity search subsequence matching applications. The framework is build on top of MESSIF (Metric Similarity Search Implementation Framework) and thus the subsequence matching algorithms can exploit advanced similarity indexes in order to significantly increase their query processing performance. To prove our concept we provide a design of query-by-example spoken term detection type of application with the usage of phonetic posteriograms and subsequence matching approach.

Parametric Modal Transition Systems

by Nikola Bene¹, Jan Køetínský, Kim Guldstrand Larsen, Mikael Moller, Jiøí Srba, A full version of the paper presented at ATVA 2011 July 2011, 24 pages.

FIMU-RS-2011-03. Available as Postscript, PDF.

Abstract:

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcome many of the limitations and we investigate the computational complexity of modal refinement checking.

Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

by Tomá¹ Brázdil, Václav Bro¾ek, Krishnendu Chatterjee, Vojtìch Forejt, Antonín Kuèera, A full version of the paper presented at conference LICS 2011. April 2011, 32 pages.

FIMU-RS-2011-02. Available as Postscript, PDF.

Abstract:

We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with k reward functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the single-objective case, both randomization and memory are necessary for strategies, and that finite-memory randomized strategies are sufficient. Under the satisfaction objective, in contrast to the single-objective case, infinite memory is necessary for strategies, and that randomized memoryless strategies are sufficient for epsilon-approximation, for all epsilon. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of reward functions, for all epsilon>0. Our results also reveal flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, correct the flaws and obtain improved results.

Human Problem Solving: Sudoku Case Study

by Radek Pelánek, A full version of a paper presented at the 24th Florida Artificial Intelligence Research Society Conference January 2011, 21 pages.

FIMU-RS-2011-01. Available as Postscript, PDF.

Abstract:

We discuss and evaluate metrics for difficulty rating of Sudoku puzzles. The correlation coefficient with human performance for our best metric is 0.95. The data on human performance were obtained from three web portals and they comprise thousands of hours of human solving over 2000 problems. We provide a simple computational model of human solving activity and evaluate it over collected data. Using the model we show that there are two sources of problem difficulty: complexity of individual steps (logic operations) and structure of dependency among steps. Beside providing a very good Sudoku-tuned metric, we also discuss a metric with few Sudoku-specific details, which still provides good results (correlation coefficient is 0.88). Hence we believe that the approach should be applicable to difficulty rating of other constraint satisfaction problems. This technical report is a full version of a paper presented at the 24th Florida Artificial Intelligence Research Society Conference.