-
The Open Porous Media Flow Reservoir Simulator
Authors:
Atgeirr Flø Rasmussen,
Tor Harald Sandve,
Kai Bao,
Andreas Lauser,
Joakim Hove,
Bård Skaflestad,
Robert Klöfkorn,
Markus Blatt,
Alf Birger Rustad,
Ove Sævareid,
Knut-Andreas Lie,
Andreas Thune
Abstract:
The Open Porous Media (OPM) initiative is a community effort that encourages open innovation and reproducible research for simulation of porous media processes. OPM coordinates collaborative software development, maintains and distributes open-source software and open data sets, and seeks to ensure that these are available under a free license in a long-term perspective.
In this paper, we presen…
▽ More
The Open Porous Media (OPM) initiative is a community effort that encourages open innovation and reproducible research for simulation of porous media processes. OPM coordinates collaborative software development, maintains and distributes open-source software and open data sets, and seeks to ensure that these are available under a free license in a long-term perspective.
In this paper, we present OPM Flow, which is a reservoir simulator developed for industrial use, as well as some of the individual components used to make OPM Flow. The descriptions apply to the 2019.10 release of OPM.
△ Less
Submitted 4 October, 2019;
originally announced October 2019.
-
Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which…
▽ More
We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with the FO^2[<,suc] alternation hierarchy.
△ Less
Submitted 28 December, 2012;
originally announced December 2012.
-
The Join of the Varieties of R-trivial and L-trivial Monoids via Combinatorics on Words
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
The join of two varieties is the smallest variety containing both. In finite semigroup theory, the varieties of R-trivial and L-trivial monoids are two of the most prominent classes of finite monoids. Their join is known to be decidable due to a result of Almeida and Azevedo. In this paper, we give a new proof for Almeida and Azevedo's effective characterization of the join of R-trivial and L-triv…
▽ More
The join of two varieties is the smallest variety containing both. In finite semigroup theory, the varieties of R-trivial and L-trivial monoids are two of the most prominent classes of finite monoids. Their join is known to be decidable due to a result of Almeida and Azevedo. In this paper, we give a new proof for Almeida and Azevedo's effective characterization of the join of R-trivial and L-trivial monoids. This characterization is a single identity of omega-terms using three variables.
△ Less
Submitted 27 June, 2012; v1 submitted 24 April, 2012;
originally announced April 2012.
-
The Join Levels of the Trotter-Weil Hierarchy are Decidable
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
The variety DA of finite monoids has a huge number of different characterizations, ranging from two-variable first-order logic FO^2 to unambiguous polynomials. In order to study the structure of the subvarieties of DA, Trotter and Weil considered the intersection of varieties of finite monoids with bands, i.e., with idempotent monoids. The varieties of idempotent monoids are very well understood a…
▽ More
The variety DA of finite monoids has a huge number of different characterizations, ranging from two-variable first-order logic FO^2 to unambiguous polynomials. In order to study the structure of the subvarieties of DA, Trotter and Weil considered the intersection of varieties of finite monoids with bands, i.e., with idempotent monoids. The varieties of idempotent monoids are very well understood and fully classified. Trotter and Weil showed that for every band variety V there exists a unique maximal variety W inside DA such that the intersection with bands yields the given band variety V. These maximal varieties W define the Trotter-Weil hierarchy. This hierarchy is infinite and it exhausts DA; induced by band varieties, it naturally has a zigzag shape. In their paper, Trotter and Weil have shown that the corners and the intersection levels of this hierarchy are decidable.
In this paper, we give a single identity of omega-terms for every join level of the Trotter-Weil hierarchy; this yields decidability. Moreover, we show that the join levels and the subsequent intersection levels do not coincide. Almeida and Azevedo have shown that the join of R-trivial and L-trivial finite monoids is decidable; this is the first non-trivial join level of the Trotter-Weil hierarchy. We extend this result to the other join levels of the Trotter-Weil hierarchy. At the end of the paper, we give two applications. First, we show that the hierarchy of deterministic and codeterministic products is decidable. And second, we show that the direction alternation depth of unambiguous interval logic is decidable.
△ Less
Submitted 20 April, 2012;
originally announced April 2012.
-
Lattices of Logical Fragments over Words
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
This paper introduces an abstract notion of fragments of monadic second-order logic. This concept is based on purely syntactic closure properties. We show that over finite words, every logical fragment defines a lattice of languages with certain closure properties. Among these closure properties are residuals and inverse C-morphisms. Here, depending on certain closure properties of the fragment, C…
▽ More
This paper introduces an abstract notion of fragments of monadic second-order logic. This concept is based on purely syntactic closure properties. We show that over finite words, every logical fragment defines a lattice of languages with certain closure properties. Among these closure properties are residuals and inverse C-morphisms. Here, depending on certain closure properties of the fragment, C is the family of arbitrary, non-erasing, length-preserving, length-multiplying, or length-reducing morphisms. In particular, definability in a certain fragment can often be characterized in terms of the syntactic morphism. This work extends a result of Straubing in which he investigated certain restrictions of first-order logic formulae. In contrast to Straubing's model-theoretic approach, our notion of a logical fragment is purely syntactic and it does not rely on Ehrenfeucht-Fraisse games.
As motivating examples, we present (1) a fragment which captures the stutter-invariant part of piecewise-testable languages and (2) an acyclic fragment of Sigma_2. As it turns out, the latter has the same expressive power as two-variable first-order logic FO^2.
△ Less
Submitted 9 March, 2012; v1 submitted 15 February, 2012;
originally announced February 2012.
-
Around Dot-depth One
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
The dot-depth hierarchy is a classification of star-free languages. It is related to the quantifier alternation hierarchy of first-order logic over finite words. We consider fragments of languages with dot-depth 1/2 and dot-depth 1 obtained by prohibiting the specification of prefixes or suffixes. As it turns out, these language classes are in one-to-one correspondence with fragments of existentia…
▽ More
The dot-depth hierarchy is a classification of star-free languages. It is related to the quantifier alternation hierarchy of first-order logic over finite words. We consider fragments of languages with dot-depth 1/2 and dot-depth 1 obtained by prohibiting the specification of prefixes or suffixes. As it turns out, these language classes are in one-to-one correspondence with fragments of existential first-order logic without min- or max-predicate. For all fragments, we obtain effective algebraic characterizations. Moreover, we give new combinatorial proofs for the decidability of the membership problem for dot-depth 1/2 and dot-depth 1.
△ Less
Submitted 7 March, 2011;
originally announced March 2011.
-
Regular Ideal Languages and Their Boolean Combinations
Authors:
Franz Jahn,
Manfred Kufleitner,
Alexander Lauser
Abstract:
We consider ideals and Boolean combinations of ideals. For the regular languages within these classes we give expressively complete automaton models. In addition, we consider general properties of regular ideals and their Boolean combinations. These properties include effective algebraic characterizations and lattice identities.
In the main part of this paper we consider the following determinis…
▽ More
We consider ideals and Boolean combinations of ideals. For the regular languages within these classes we give expressively complete automaton models. In addition, we consider general properties of regular ideals and their Boolean combinations. These properties include effective algebraic characterizations and lattice identities.
In the main part of this paper we consider the following deterministic one-way automaton models: unions of flip automata, weak automata, and Staiger-Wagner automata. We show that each of these models is expressively complete for regular Boolean combination of right ideals. Right ideals over finite words resemble the open sets in the Cantor topology over infinite words. An omega-regular language is a Boolean combination of open sets if and only if it is recognizable by a deterministic Staiger-Wagner automaton; and our result can be seen as a finitary version of this classical theorem. In addition, we also consider the canonical automaton models for right ideals, prefix-closed languages, and factorial languages.
In the last section, we consider a two-way automaton model which is known to be expressively complete for two-variable first-order logic. We show that the above concepts can be adapted to these two-way automata such that the resulting languages are the right ideals (resp. prefix-closed languages, resp. Boolean combinations of right ideals) definable in two-variable first-order logic.
△ Less
Submitted 25 May, 2012; v1 submitted 24 February, 2011;
originally announced February 2011.
-
Languages of Dot-depth One over Infinite Words
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
Over finite words, languages of dot-depth one are expressively complete for alternation-free first-order logic. This fragment is also known as the Boolean closure of existential first-order logic. Here, the atomic formulas comprise order, successor, minimum, and maximum predicates. Knast (1983) has shown that it is decidable whether a language has dot-depth one. We extend Knast's result to infinit…
▽ More
Over finite words, languages of dot-depth one are expressively complete for alternation-free first-order logic. This fragment is also known as the Boolean closure of existential first-order logic. Here, the atomic formulas comprise order, successor, minimum, and maximum predicates. Knast (1983) has shown that it is decidable whether a language has dot-depth one. We extend Knast's result to infinite words. In particular, we describe the class of languages definable in alternation-free first-order logic over infinite words, and we give an effective characterization of this fragment. This characterization has two components. The first component is identical to Knast's algebraic property for finite words and the second component is a topological property, namely being a Boolean combination of Cantor sets.
As an intermediate step we consider finite and infinite words simultaneously. We then obtain the results for infinite words as well as for finite words as special cases. In particular, we give a new proof of Knast's Theorem on languages of dot-depth one over finite words.
△ Less
Submitted 1 April, 2011; v1 submitted 21 January, 2011;
originally announced January 2011.
-
First-order Fragments with Successor over Infinite Words
Authors:
Jakub Kallas,
Manfred Kufleitner,
Alexander Lauser
Abstract:
We consider fragments of first-order logic and as models we allow finite and infinite words simultaneously. The only binary relations apart from equality are order comparison < and the successor predicate +1. We give characterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] in terms of algebraic and topological properties. To this end we introduce the factor topology over infini…
▽ More
We consider fragments of first-order logic and as models we allow finite and infinite words simultaneously. The only binary relations apart from equality are order comparison < and the successor predicate +1. We give characterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] in terms of algebraic and topological properties. To this end we introduce the factor topology over infinite words. It turns out that a language L is in the intersection of FO2 and Sigma2 if and only if L is the interior of an FO2 language. Symmetrically, a language is in the intersection of FO2 and Pi2 if and only if it is the topological closure of an FO2 language. The fragment Delta2, which by definition is the intersection of Sigma2 and Pi2 contains exactly the clopen languages in FO2. In particular, over infinite words Delta2 is a strict subclass of FO2. Our characterizations yield decidability of the membership problem for all these fragments over finite and infinite words; and as a corollary we also obtain decidability for infinite words. Moreover, we give a new decidable algebraic characterization of dot-depth 3/2 over finite words. Decidability of dot-depth 3/2 over finite words was first shown by Glaßer and Schmitz in STACS 2000, and decidability of the membership problem for FO2 over infinite words was shown 1998 by Wilke in his habilitation thesis whereas decidability of Sigma2 over infinite words was not known before.
△ Less
Submitted 30 December, 2010;
originally announced January 2011.
-
Partially Ordered Two-way Büchi Automata
Authors:
Manfred Kufleitner,
Alexander Lauser
Abstract:
We introduce partially ordered two-way Büchi automata and characterize their expressive power in terms of fragments of first-order logic FO[<]. Partially ordered two-way Büchi automata are Büchi automata which can change the direction in which the input is processed with the constraint that whenever a state is left, it is never re-entered again. Nondeterministic partially ordered two-way Büchi aut…
▽ More
We introduce partially ordered two-way Büchi automata and characterize their expressive power in terms of fragments of first-order logic FO[<]. Partially ordered two-way Büchi automata are Büchi automata which can change the direction in which the input is processed with the constraint that whenever a state is left, it is never re-entered again. Nondeterministic partially ordered two-way Büchi automata coincide with the first-order fragment Sigma2. Our main contribution is that deterministic partially ordered two-way Büchi automata are expressively complete for the first-order fragment Delta2. As an intermediate step, we show that deterministic partially ordered two-way Büchi automata are effectively closed under Boolean operations.
A small model property yields coNP-completeness of the emptiness problem and the inclusion problem for deterministic partially ordered two-way Büchi automata.
△ Less
Submitted 25 August, 2011; v1 submitted 14 June, 2010;
originally announced June 2010.
-
Rankers over Infinite Words
Authors:
Luc Dartois,
Manfred Kufleitner,
Alexander Lauser
Abstract:
We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite word…
▽ More
We consider the four fragments FO2, the intersection of Sigma2 and FO2, the intersection of Pi2 and FO2, and Delta2 of first-order logic FO[<] over finite and infinite words. For all four fragments, we give characterizations in terms of rankers. In particular, we generalize the notion of a ranker to infinite words in two possible ways. Both extensions are natural in the sense that over finite words, they coincide with classical rankers and over infinite words, they both have the full expressive power of FO2. Moreover, the first extension of rankers admits a characterization of the intersection of Sigma2 and FO2 while the other leads to a characterization of the intersection of Pi2 and FO2. Both versions of rankers yield characterizations of the fragment Delta2. As a byproduct, we also obtain characterizations based on unambiguous temporal logic and unambiguous interval temporal logic.
△ Less
Submitted 4 May, 2010;
originally announced May 2010.
