-
On the determinization of event-clock input-driven pushdown automata
Authors:
Mizuhito Ogawa,
Alexander Okhotin
Abstract:
Input-driven pushdown automata (also known as visibly pushdown automata and as nested word automata) are a subclass of deterministic pushdown automata and a superclass of the parenthesis languages. Nguyen and Ogawa ("Event-clock visibly pushdown automata", SOFSEM 2009) defined a timed extension of these automata under the event-clock model, and showed that this model can be determinized using the…
▽ More
Input-driven pushdown automata (also known as visibly pushdown automata and as nested word automata) are a subclass of deterministic pushdown automata and a superclass of the parenthesis languages. Nguyen and Ogawa ("Event-clock visibly pushdown automata", SOFSEM 2009) defined a timed extension of these automata under the event-clock model, and showed that this model can be determinized using the method of region construction. This paper defines a further extension of this model with the event clock on the call-return operations, and proposes a new, direct determinization procedure for these automata: an $n$-state nondeterministic automaton with $k$ different clock constraints is transformed to a deterministic automaton with $2^{n^2}$ states, $2^{n^2+k}$ stack symbols and the same clock constraints as in the original automaton. The construction is shown to be asymptotically optimal with respect to both the number of states and the number of stack symbols.
△ Less
Submitted 6 March, 2021;
originally announced March 2021.
-
Personalized Classifier for Food Image Recognition
Authors:
Shota Horiguchi,
Sosuke Amano,
Makoto Ogawa,
Kiyoharu Aizawa
Abstract:
Currently, food image recognition tasks are evaluated against fixed datasets. However, in real-world conditions, there are cases in which the number of samples in each class continues to increase and samples from novel classes appear. In particular, dynamic datasets in which each individual user creates samples and continues the updating process often have content that varies considerably between…
▽ More
Currently, food image recognition tasks are evaluated against fixed datasets. However, in real-world conditions, there are cases in which the number of samples in each class continues to increase and samples from novel classes appear. In particular, dynamic datasets in which each individual user creates samples and continues the updating process often have content that varies considerably between different users, and the number of samples per person is very limited. A single classifier common to all users cannot handle such dynamic data. Bridging the gap between the laboratory environment and the real world has not yet been accomplished on a large scale. Personalizing a classifier incrementally for each user is a promising way to do this. In this paper, we address the personalization problem, which involves adapting to the user's domain incrementally using a very limited number of samples. We propose a simple yet effective personalization framework which is a combination of the nearest class mean classifier and the 1-nearest neighbor classifier based on deep features. To conduct realistic experiments, we made use of a new dataset of daily food images collected by a food-logging application. Experimental results show that our proposed method significantly outperforms existing methods.
△ Less
Submitted 8 April, 2018;
originally announced April 2018.
-
Subtropical Satisfiability
Authors:
Pascal Fontaine,
Mizuhito Ogawa,
Thomas Sturm,
Xuan Tung Vu
Abstract:
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced i…
▽ More
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.
△ Less
Submitted 28 June, 2017;
originally announced June 2017.
-
Confluence of Layered Rewrite Systems
Authors:
Jean-Pierre Jouannaud,
Jiaxiang Liu,
Mizuhito Ogawa
Abstract:
We investigate the new, Turing-complete class of layered systems, whose lefthand sides of rules can only be overlapped at a multiset of disjoint or equal positions. Layered systems define a natural notion of rank for terms: the maximal number of non-overlap** redexes along a path from the root to a leaf. Overlap**s are allowed in finite or infinite trees. Rules may be non-terminating, non-left…
▽ More
We investigate the new, Turing-complete class of layered systems, whose lefthand sides of rules can only be overlapped at a multiset of disjoint or equal positions. Layered systems define a natural notion of rank for terms: the maximal number of non-overlap** redexes along a path from the root to a leaf. Overlap**s are allowed in finite or infinite trees. Rules may be non-terminating, non-left-linear, or non-right-linear. Using a novel unification technique, cyclic unification, and the so-alled subrewriting relation, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.
△ Less
Submitted 15 September, 2015;
originally announced September 2015.
