-
Let's Get the FACS Straight -- Reconstructing Obstructed Facial Features
Authors:
Tim Büchner,
Sven Sickert,
Gerd Fabian Volk,
Christoph Anders,
Orlando Guntinas-Lichius,
Joachim Denzler
Abstract:
The human face is one of the most crucial parts in interhuman communication. Even when parts of the face are hidden or obstructed the underlying facial movements can be understood. Machine learning approaches often fail in that regard due to the complexity of the facial structures. To alleviate this problem a common approach is to fine-tune a model for such a specific application. However, this is…
▽ More
The human face is one of the most crucial parts in interhuman communication. Even when parts of the face are hidden or obstructed the underlying facial movements can be understood. Machine learning approaches often fail in that regard due to the complexity of the facial structures. To alleviate this problem a common approach is to fine-tune a model for such a specific application. However, this is computational intensive and might have to be repeated for each desired analysis task. In this paper, we propose to reconstruct obstructed facial parts to avoid the task of repeated fine-tuning. As a result, existing facial analysis methods can be used without further changes with respect to the data. In our approach, the restoration of facial features is interpreted as a style transfer task between different recording setups. By using the CycleGAN architecture the requirement of matched pairs, which is often hard to fullfill, can be eliminated. To proof the viability of our approach, we compare our reconstructions with real unobstructed recordings. We created a novel data set in which 36 test subjects were recorded both with and without 62 surface electromyography sensors attached to their faces. In our evaluation, we feature typical facial analysis tasks, like the computation of Facial Action Units and the detection of emotions. To further assess the quality of the restoration, we also compare perceptional distances. We can show, that scores similar to the videos without obstructing sensors can be achieved.
△ Less
Submitted 10 November, 2023; v1 submitted 9 November, 2023;
originally announced November 2023.
-
Efficient Normalization of Linear Temporal Logic
Authors:
Javier Esparza,
Rubén Rubio,
Salomon Sickert
Abstract:
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F}\, \varphi_i \vee \mathbf{F}\mathbf{G}\, ψ_i $, where $\varphi_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this resu…
▽ More
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F}\, \varphi_i \vee \mathbf{F}\mathbf{G}\, ψ_i $, where $\varphi_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalization procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present direct and purely syntactic normalization procedures for LTL, yielding a normal form very similar to the one by Chang, Manna, and Pnueli, that exhibit only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalizes the formula, translates it into a special very weak alternating automaton, and applies a simple determinization procedure, valid only for these special automata.
△ Less
Submitted 27 February, 2024; v1 submitted 19 October, 2023;
originally announced October 2023.
-
A Simple Rewrite System for the Normalization of Linear Temporal Logic
Authors:
Javier Esparza,
Ruben Rubio,
Salomon Sickert
Abstract:
In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of Past LTL (the extension of Linear Temporal Logic with past operators) is equivalent to a conjunction of formulas of the form $\mathbf{G}\mathbf{F} \varphi \vee \mathbf{F}\mathbf{G} ψ$, where $\varphi$ and $ψ$ contain only past operators. Some years later, Chang, Manna, and Pnueli derived a similar normal form for LTL. Both…
▽ More
In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of Past LTL (the extension of Linear Temporal Logic with past operators) is equivalent to a conjunction of formulas of the form $\mathbf{G}\mathbf{F} \varphi \vee \mathbf{F}\mathbf{G} ψ$, where $\varphi$ and $ψ$ contain only past operators. Some years later, Chang, Manna, and Pnueli derived a similar normal form for LTL. Both normalization procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. In 2020, Sickert and Esparza presented a direct and purely syntactic normalization procedure for LTL yielding a normal form similar to the one by Chang, Manna, and Pnueli, with a single exponential blow-up, and applied it to the problem of constructing a succinct deterministic $ω$-automaton for a given formula. However, their procedure had exponential time complexity in the best case. In particular, it does not perform better for formulas that are almost in normal form. In this paper we present an alternative normalization procedure based on a simple set of rewrite rules.
△ Less
Submitted 18 April, 2023;
originally announced April 2023.
-
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Authors:
Swen Jacobs,
Guillermo A. Perez,
Remco Abraham,
Veronique Bruyere,
Michael Cadilhac,
Maximilien Colange,
Charly Delfosse,
Tom van Dijk,
Alexandre Duret-Lutz,
Peter Faymonville,
Bernd Finkbeiner,
Ayrat Khalimov,
Felix Klein,
Michael Luttenberger,
Klara Meyer,
Thibaud Michaud,
Adrien Pommellet,
Florian Renkin,
Philipp Schlehuber-Caissier,
Mouhammad Sakr,
Salomon Sickert,
Gaetan Staquet,
Clement Tamines,
Leander Tentrup,
Adam Walker
Abstract:
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, inclu…
▽ More
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality - that is, the total size in terms of logic and memory elements - of solutions.
△ Less
Submitted 6 May, 2024; v1 submitted 1 June, 2022;
originally announced June 2022.
-
On the Translation of Automata to Linear Temporal Logic
Authors:
Udi Boker,
Karoliina Lehtinen,
Salomon Sickert
Abstract:
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic $ω$-regular automata to LTL. Our first contribution consists of tight bounds for LTL over a unary alphabet: alter…
▽ More
While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic $ω$-regular automata to LTL. Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consists of a translation of general counter-free deterministic $ω$-regular automata into LTL formulas of double exponential temporal-nesting depth and triple exponential length, using an intermediate Krohn-Rhodes cascade decomposition of the automaton. To our knowledge, this is the first elementary bound on this translation. Furthermore, our translation preserves the acceptance condition of the automaton in the sense that it turns a loo**, weak, Büchi, coBüchi or Muller automaton into a formula that belongs to the matching class of the syntactic future hierarchy. In particular, it can be used to translate an LTL formula recognising a safety language to a formula belonging to the safety fragment of LTL (over both finite and infinite words).
△ Less
Submitted 8 May, 2022; v1 submitted 25 January, 2022;
originally announced January 2022.
-
Certifying DFA Bounds for Recognition and Separation
Authors:
Orna Kupferman,
Nir Lavee,
Salomon Sickert
Abstract:
The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a deterministic finite automaton (DFA) needs in order to recognize a given language. Given a language $L$ and a bound $k$, recognizability of $L$ by a DFA with $k$ states is…
▽ More
The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a deterministic finite automaton (DFA) needs in order to recognize a given language. Given a language $L$ and a bound $k$, recognizability of $L$ by a DFA with $k$ states is reduced to a game between Prover and Refuter. The interaction along the game then serves as a certificate. Certificates generated by Prover are minimal DFAs. Certificates generated by Refuter are faulty attempts to define the required DFA. We compare the length of offline certificates, which are generated with no interaction between Prover and Refuter, and online certificates, which are based on such an interaction, and are thus shorter. We show that our approach is useful also for certification of separability of regular languages by a DFA of a given size. Unlike DFA minimization, which can be solved in polynomial time, separation is NP-complete, and thus the certification approach is essential. In addition, we prove NP-completeness of a strict version of separation.
△ Less
Submitted 4 July, 2021;
originally announced July 2021.
-
Certifying Inexpressibility
Authors:
Orna Kupferman,
Salomon Sickert
Abstract:
Different classes of automata on infinite words have different expressive power. Deciding whether a given language $L \subseteq Σ^ω$ can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in $Σ$, and Prover responds with an annotation of the current state of the run (for example, in the c…
▽ More
Different classes of automata on infinite words have different expressive power. Deciding whether a given language $L \subseteq Σ^ω$ can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in $Σ$, and Prover responds with an annotation of the current state of the run (for example, in the case of Büchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is). Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in $L$. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates. Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata. In addition, it can be used for refuting separation of two languages by an automaton of the desired class, and for finding automata that approximate $L$ and belong to the desired class.
△ Less
Submitted 19 February, 2021; v1 submitted 21 January, 2021;
originally announced January 2021.
-
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
Authors:
Salomon Sickert,
Javier Esparza
Abstract:
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} \varphi_i \vee \mathbf{F}\mathbf{G} ψ_i$, where $\varphi_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to…
▽ More
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} \varphi_i \vee \mathbf{F}\mathbf{G} ψ_i$, where $\varphi_i$ and $ψ_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.
△ Less
Submitted 1 May, 2020;
originally announced May 2020.
-
Facial Behavior Analysis using 4D Curvature Statistics for Presentation Attack Detection
Authors:
Martin Thümmel,
Sven Sickert,
Joachim Denzler
Abstract:
The human face has a high potential for biometric identification due to its many individual traits. At the same time, such identification is vulnerable to biometric copies. These presentation attacks pose a great challenge in unsupervised authentication settings. As a countermeasure, we propose a method that automatically analyzes the plausibility of facial behavior based on a sequence of 3D face…
▽ More
The human face has a high potential for biometric identification due to its many individual traits. At the same time, such identification is vulnerable to biometric copies. These presentation attacks pose a great challenge in unsupervised authentication settings. As a countermeasure, we propose a method that automatically analyzes the plausibility of facial behavior based on a sequence of 3D face scans. A compact feature representation measures facial behavior using the temporal curvature change. Finally, we train our method only on genuine faces in an anomaly detection scenario. Our method can detect presentation attacks using elastic 3D masks, bent photographs with eye holes, and monitor replay-attacks. For evaluation, we recorded a challenging database containing such cases using a high-quality 3D sensor. It features 109 4D face scans including eleven different types of presentation attacks. We achieve error rates of 11% and 6% for APCER and BPCER, respectively.
△ Less
Submitted 10 August, 2021; v1 submitted 14 October, 2019;
originally announced October 2019.
-
The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
Authors:
Swen Jacobs,
Roderick Bloem,
Maximilien Colange,
Peter Faymonville,
Bernd Finkbeiner,
Ayrat Khalimov,
Felix Klein,
Michael Luttenberger,
Philipp J. Meyer,
Thibaud Michaud,
Mouhammad Sakr,
Salomon Sickert,
Leander Tentrup,
Adam Walker
Abstract:
We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the evaluation scheme and the experimental setup of SYNTCOMP 2018. We give an overview of the participants of SYNTCOMP 2018 and highlight changes compared to previous years. Finally, we present and analyze the results of o…
▽ More
We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the evaluation scheme and the experimental setup of SYNTCOMP 2018. We give an overview of the participants of SYNTCOMP 2018 and highlight changes compared to previous years. Finally, we present and analyze the results of our experimental evaluation, including a ranking of tools with respect to quantity and quality of solutions.
△ Less
Submitted 15 April, 2019;
originally announced April 2019.
-
Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
Authors:
Michael Luttenberger,
Philipp J. Meyer,
Salomon Sickert
Abstract:
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the s…
▽ More
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.
△ Less
Submitted 30 October, 2019; v1 submitted 29 March, 2019;
originally announced March 2019.
-
LTL Store: Repository of LTL formulae from literature and case studies
Authors:
Jan Křetínský,
Tobias Meggendorfer,
Salomon Sickert
Abstract:
This continuously extended technical report collects and compares commonly used formulae from the literature and provides them in a machine readable way.
This continuously extended technical report collects and compares commonly used formulae from the literature and provides them in a machine readable way.
△ Less
Submitted 29 June, 2018;
originally announced July 2018.
-
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
Authors:
Javier Esparza,
Jan Kretinsky,
Salomon Sickert
Abstract:
We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language…
▽ More
We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed.
△ Less
Submitted 2 May, 2018;
originally announced May 2018.
-
LTL to Deterministic Emerson-Lei Automata
Authors:
David Müller,
Salomon Sickert
Abstract:
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure allows the shift of complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction tha…
▽ More
We introduce a new translation from linear temporal logic (LTL) to deterministic Emerson-Lei automata, which are omega-automata with a Muller acceptance condition symbolically expressed as a Boolean formula. The richer acceptance condition structure allows the shift of complexity from the state space to the acceptance condition. Conceptually the construction is an enhanced product construction that exploits knowledge of its components to reduce the number of states. We identify two fragments of LTL, for which one can easily construct deterministic automata and show how knowledge of these components can reduce the number of states. We extend this idea to a general LTL framework, where we can use arbitrary LTL to deterministic automata translators for parts of formulas outside the mentioned fragments. Further, we show succinctness of the translation compared to existing construction. The construction is implemented in the tool Delag, which we evaluate on several benchmarks of LTL formulas and probabilistic model checking case studies.
△ Less
Submitted 7 September, 2017;
originally announced September 2017.
-
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
Authors:
Javier Esparza,
Jan Křetínský,
Jean-François Raskin,
Salomon Sickert
Abstract:
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formu…
▽ More
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, \enquote{Safraless} LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.
△ Less
Submitted 21 January, 2017;
originally announced January 2017.
-
Neither Quick Nor Proper -- Evaluation of QuickProp for Learning Deep Neural Networks
Authors:
Clemens-Alexander Brust,
Sven Sickert,
Marcel Simon,
Erik Rodner,
Joachim Denzler
Abstract:
Neural networks and especially convolutional neural networks are of great interest in current computer vision research. However, many techniques, extensions, and modifications have been published in the past, which are not yet used by current approaches. In this paper, we study the application of a method called QuickProp for training of deep neural networks. In particular, we apply QuickProp duri…
▽ More
Neural networks and especially convolutional neural networks are of great interest in current computer vision research. However, many techniques, extensions, and modifications have been published in the past, which are not yet used by current approaches. In this paper, we study the application of a method called QuickProp for training of deep neural networks. In particular, we apply QuickProp during learning and testing of fully convolutional networks for the task of semantic segmentation. We compare QuickProp empirically with gradient descent, which is the current standard method. Experiments suggest that QuickProp can not compete with standard gradient descent techniques for complex computer vision tasks like semantic segmentation.
△ Less
Submitted 15 June, 2016; v1 submitted 14 June, 2016;
originally announced June 2016.
-
Convolutional Patch Networks with Spatial Prior for Road Detection and Urban Scene Understanding
Authors:
Clemens-Alexander Brust,
Sven Sickert,
Marcel Simon,
Erik Rodner,
Joachim Denzler
Abstract:
Classifying single image patches is important in many different applications, such as road detection or scene understanding. In this paper, we present convolutional patch networks, which are convolutional networks learned to distinguish different image patches and which can be used for pixel-wise labeling. We also show how to incorporate spatial information of the patch as an input to the network,…
▽ More
Classifying single image patches is important in many different applications, such as road detection or scene understanding. In this paper, we present convolutional patch networks, which are convolutional networks learned to distinguish different image patches and which can be used for pixel-wise labeling. We also show how to incorporate spatial information of the patch as an input to the network, which allows for learning spatial priors for certain categories jointly with an appearance model. In particular, we focus on road detection and urban scene understanding, two application areas where we are able to achieve state-of-the-art results on the KITTI as well as on the LabelMeFacade dataset.
Furthermore, our paper offers a guideline for people working in the area and desperately wandering through all the painstaking details that render training CNs on image patches extremely difficult.
△ Less
Submitted 23 February, 2015;
originally announced February 2015.
-
On Refinements of Boolean and Parametric Modal Transition Systems
Authors:
Jan Křetínský,
Salomon Sickert
Abstract:
We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the refinement problems over both classes. Firstly, we reduce the problem of modal refinement over both classes to a problem solvable by a QBF solver and provide experimental results showing our technique scales well. Secondly, we extend the algorithm for thorough refinement of MT…
▽ More
We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the refinement problems over both classes. Firstly, we reduce the problem of modal refinement over both classes to a problem solvable by a QBF solver and provide experimental results showing our technique scales well. Secondly, we extend the algorithm for thorough refinement of MTS providing better complexity then via reductions to previously studied problems. Finally, we investigate the relationship between modal and thorough refinement on the two classes and show how the thorough refinement can be approximated by the modal refinement.
△ Less
Submitted 18 April, 2013;
originally announced April 2013.
