Local abstraction–refinement for the <Emphasis Type="Italic">μ</Emphasis>-calculus

A key technique for the verification of programs is counterexample-guided abstraction–refinement (CEGAR). Grumberg et al. (LNCS, vol 3385, pp. 233–249. Springer, Berlin, 2005; Inf Comput 205(8):1130–1148, 2007) developed a CEGAR-based algorithm for the modal μ-calculus. There, every abstract state is split in a refinement step. In this paper, the work of Grumberg et al. is generalized by presenting a new CEGAR-based algorithm for the μ-calculus. It is based on a more expressive abstract model and applies refinement only locally (at a single abstract state), i.e., the lazy abstraction technique for safety properties is adapted to the μ-calculus. Furthermore, it separates refinement determination from the (3-valued based) model checking. Three different heuristics for refinement determination are presented and illustrated.     

Lower-bound-constrained runs in weighted timed automata

We investigate a number of problems related to infinite runs of weighted timed automata (with a single weight variable), subject to lower-bound constraints on the accumulated weight. Closing an open problem from Bouyer et al. (2008), we show that the existence of an infinite lower-bound-constrained run is—for us somewhat unexpectedly—undecidable for weighted timed automata with four or more clocks.This undecidability result assumes a fixed and known initial credit. We show that the related problem of existence of an initial credit for which there exists a feasible run is decidable in PSPACE. We also investigate the variant of these problems where only bounded-duration runs are considered, showing that this restriction makes our original problem decidable in  NEXPTIME. We prove that the universal versions of all those problems (i.e, checking that all the considered runs satisfy the lower-bound constraint) are decidable in PSPACE.Finally, we extend this study to multi-weighted timed automata: the existence of a feasible run becomes undecidable even for bounded duration, but the existence of initial credits remains decidable (in PSPACE).     

Updatable timed automata with one updatable clock

Updatable timed automata (UTAs) proposed by Bouyer et.al., is an extension of timed automata (TAs) having the extra ability to update clocks in a more elaborate way than simply reset them to zero. The reachability of UTAs is generally undecidable, which can be easily gained by regarding a pair of clocks as updatable counters. This paper investigates a subclass of UTAs by restricting the number of updatable clocks to be one. We will show that (1) the reachability of general UTAs with one updatable clock (UTA1s) is still undecidable, and (2) that of UTA1s under diagonal-free constraints is decidable, and the complexity is Pspace-complete. The former is achieved by encoding Minsky machines to the general UTA1s, where two counters are simulated by the updatable clock. The latter is gained by regarding a region of a UTA1 to be an unbounded digiword, and encoding sets of digiwords that are accepted by a one counter automaton where regions are generated as the value of the counter.     

On Aperiodic and Star-Free Formal Power Series in Partially Commuting Variables

Formal power series over non-commuting variables have been investigated as representations of the behavior of automata with multiplicities. Here we introduce and investigate the concepts of aperiodic and of star-free formal power series over semirings and partially commuting variables. We prove that if the semiring K is idempotent and commutative, or if K is idempotent and the variables are non-commuting, then the product of any two aperiodic series is again aperiodic. We also show that if K is idempotent and the matrix monoids over K have a Burnside property (satisfied, e.g. by the tropical semiring), then the aperiodic and the star-free series coincide. This generalizes a classical result of Schützenberger (Inf. Control 4:245–270, 1961) for aperiodic regular languages and subsumes a result of Guaiana et al. (Theor. Comput. Sci. 97:301–311, 1992) on aperiodic trace languages. This work partly supported by the DAAD-PROCOPE project Temporal and Quantitative Analysis of Distributed Systems.     

Approximation Algorithms for Reconstructing the Duplication History of Tandem Repeats

Computing the duplication history of a tandem repeated region is an important problem in computational biology (Fitch in Genetics 86:623–644, 1977; Jaitly et al. in J. Comput. Syst. Sci. 65:494–507, 2002; Tang et al. in J. Comput. Biol. 9:429–446, 2002). In this paper, we design a polynomial-time approximation scheme (PTAS) for the case where the size of the duplication block is 1. Our PTAS is faster than the previously best PTAS in Jaitly et al. (J. Comput. Syst. Sci. 65:494–507, 2002). For example, to achieve a ratio of 1.5, our PTAS takes O(n ⁵) time while the PTAS in Jaitly et al. (J. Comput. Syst. Sci. 65:494–507, 2002) takes O(n ¹¹) time. We also design a ratio-6 polynomial-time approximation algorithm for the case where the size of each duplication block is at most 2. This is the first polynomial-time approximation algorithm with a guaranteed ratio for this case. Part of work was done during a Z.-Z. Chen visit at City University of Hong Kong.     

An improved data hiding approach for polygon meshes

We present an improved technique for data hiding in polygonal meshes, which is based on the work of Bogomjakov et al. (Comput. Graph. Forum 27(2):637–642, 2008). Like their method, we use an arrangement on primitives relative to a reference ordering to embed a message. But instead of directly interpreting the index of a primitive in the reference ordering as the encoded/decoded bits, our method slightly modifies the mapping so that our modification doubles the chance of encoding an additional bit compared to Bogomjakov et al.’s (Comput. Graph. Forum 27(2):637–642, 2008). We illustrate the inefficiency in the original mapping of Bogomjakov et al. (Comput. Graph. Forum 27(2):637–642, 2008) with an intuitive representation using a binary tree.     

On Total Variation Minimization and Surface Evolution Using Parametric Maximum Flows

In a recent paper Boykov et al. (LNCS, Vol. 3953, pp. 409–422, 2006) propose an approach for computing curve and surface evolution using a variational approach and the geo-cuts method of Boykov and Kolmogorov (International conference on computer vision, pp. 26–33, 2003). We recall in this paper how this is related to well-known approaches for mean curvature motion, introduced by Almgren et al. (SIAM Journal on Control and Optimization 31(2):387–438, 1993) and Luckhaus and Sturzenhecker (Calculus of Variations and Partial Differential Equations 3(2):253–271, 1995), and show how the corresponding problems can be solved with sub-pixel accuracy using Parametric Maximum Flow techniques. This provides interesting algorithms for computing crystalline curvature motion, possibly with a forcing term. A. Chambolle’s research supported by ANR project “MICA”, grant ANR-08-BLAN-0082. J. Darbon’s research supported by ONR grant N000140710810.     

Event clock message passing automata: a logical characterization and an emptiness checking algorithm

We are interested in modeling behaviors and verifying properties of systems in which time and concurrency play a crucial role. We introduce a model of distributed automata which are equipped with event clocks as in Alur et al. (Theor Comput Sci 211:253–273, 1999), which we call Event Clock Message Passing Automata (ECMPA). To describe the behaviors of such systems we use timed partial orders (modeled as message sequence charts with timing). Our first goal is to extend the classical Büchi-Elgot-Trakhtenbrot equivalence to the timed and distributed setting, by showing an equivalence between ECMPA and a timed extension of monadic second-order (MSO) logic. We obtain such a constructive equivalence in two different ways: (1) by restricting the semantics by bounding the set of timed partial orders; (2) by restricting the timed MSO logic to its existential fragment. We next consider the emptiness problem for ECMPA, which asks if a given ECMPA has some valid timed execution. In general this problem is undecidable and we show that by considering only bounded timed executions, we can obtain decidability. We do this by constructing a timed automaton which accepts all bounded timed executions of the ECMPA and checking emptiness of this timed automaton.     

A posteriori error analysis of time-dependent Stokes problem by Chorin-Temam scheme

We present a posteriori-residual analysis for the approximate time-dependent Stokes model Chorin-Temam projection scheme (Chorin in Math. Comput. 23:341–353, 1969; Temam in Arch. Ration. Mech. Appl. 33:377–385, 1969). Based on the multi-step approach introduced in Bergam et al. (Math. Comput. 74(251):1117–1138, 2004), we derive error estimators, with respect to both time and space approximations, related to diffusive and incompressible parts of Stokes equations. Using a conforming finite element discretization, we prove the equivalence between error and estimators under specific conditions.     

A note on the alternating group network

The class of alternating group networks was introduced in the late 1990’s as an alternative to the alternating group graphs as interconnection networks. Recently, additional properties for the alternating group networks have been published. In particular, Zhou et al., J. Supercomput (2009), doi:, was published very recently in this journal. We show that this so-called new interconnection topology is in fact isomorphic to the (n,n−2)-star, a member of the well-known (n,k)-stars, 1≤k≤n−1, a class of popular networks proposed earlier for which a large amount of work have already been done. Specifically, the problem in Zhou et al., J. Supercomput (2009), doi:, was addressed in Lin and Duh, Inf. Sci. 178(3), 788–801, 2008, when k = n−2.     

A New Mapped Weighted Essentially Non-oscillatory Scheme

The weighted essentially non-oscillatory (WENO) methods are a popular high-order spatial discretization for hyperbolic partial differential equations. Recently Henrick et al. (J. Comput. Phys. 207:542–567, 2005) noted that the fifth-order WENO method by Jiang and Shu (J. Comput. Phys. 126:202–228, 1996) is only third-order accurate near critical points of the smooth regions in general. Using a simple mapping function to the original weights in Jiang and Shu (J. Comput. Phys. 126:202–228, 1996), Henrick et al. developed a mapped WENO method to achieve the optimal order of accuracy near critical points. In this paper we study the mapped WENO scheme and find that, when it is used for solving the problems with discontinuities, the mapping function in Henrick et al. (J. Comput. Phys. 207:542–567, 2005) may amplify the effect from the non-smooth stencils and thus cause a potential loss of accuracy near discontinuities. This effect may be difficult to be observed for the fifth-order WENO method unless a long time simulation is desired. However, if the mapping function is applied to seventh-order WENO methods (Balsara and Shu in J. Comput. Phys. 160:405–452, 2000), the error can increase much faster so that it can be observed with a moderate output time. In this paper a new mapping function is proposed to overcome this potential loss of accuracy.     

Characteristic-Based Schemes for Multi-Class Lighthill-Whitham-Richards Traffic Models

In this paper we provide the full spectral decomposition of the Multi-Class Lighthill Whitham Richards (MCLWR) traffic models described in (Wong et al. in Transp. Res. Part A 36:827–841, 2002; Benzoni-Gavage and Colombo in Eur. J. Appl. Math. 14:587–612, 2003). Even though the eigenvalues of these models can only be found numerically, the knowledge of the spectral structure allows the use of characteristic-based High Resolution Shock Capturing (HRSC) schemes. We compare the characteristic-based approach to the component-wise schemes used in (Zhang et al. in J. Comput. Phys. 191:639–659, 2003), and propose two strategies to minimize the oscillatory behavior that can be observed when using the component-wise approach.     

All-Pairs Shortest Paths with Real Weights in <Emphasis Type="Italic">O</Emphasis>(<Emphasis Type="Italic">n</Emphasis><Superscript>3</Superscript>/log <Emphasis Type="Italic">n</Emphasis>) Time

We describe an O(n ³/log n)-time algorithm for the all-pairs-shortest-paths problem for a real-weighted directed graph with n vertices. This slightly improves a series of previous, slightly subcubic algorithms by Fredman (SIAM J. Comput. 5:49–60, 1976), Takaoka (Inform. Process. Lett. 43:195–199, 1992), Dobosiewicz (Int. J. Comput. Math. 32:49–60, 1990), Han (Inform. Process. Lett. 91:245–250, 2004), Takaoka (Proc. 10th Int. Conf. Comput. Comb., Lect. Notes Comput. Sci., vol. 3106, pp. 278–289, Springer, 2004), and Zwick (Proc. 15th Int. Sympos. Algorithms and Computation, Lect. Notes Comput. Sci., vol. 3341, pp. 921–932, Springer, 2004). The new algorithm is surprisingly simple and different from previous ones. A preliminary version of this paper appeared in Proc. 9th Workshop Algorithms Data Struct. (WADS), Lect. Notes Comput. Sci., vol. 3608, pp. 318–324, Springer, 2005.     

Solving steel mill slab design problems

The steel mill slab design problem from the CSPLIB is a combinatorial optimization problem motivated by an application of the steel industry. It has been widely studied in the constraint programming community. Several methods were proposed to solve this problem. A steel mill slab library was created which contains 380 instances. A closely related binpacking problem called the multiple knapsack problem with color constraints, originated from the same industrial problem, was discussed in the integer programming community. In particular, a simple integer program for this problem has been given by Forrest et al. (INFORMS J Comput 18:129–134, 2006). The aim of this paper is to bring these different studies together. Moreover, we adapt the model of Forrest et al. (INFORMS J Comput 18:129–134, 2006) for the steel mill slab design problem. Using this model and a state-of-the-art integer program solver all instances of the steel mill slab library can be solved efficiently to optimality. We improved, thereby, the solution values of 76 instances compared to previous results (Schaus et al., Constraints 16:125–147, 2010). Finally, we consider a recently introduced variant of the steel mill slab design problem, where within all solutions which minimize the leftover one is interested in a solution which requires a minimum number of slabs. For that variant we introduce two approaches and solve all instances of the steel mill slab library with this slightly changed objective function to optimality.     

The Directed Orienteering Problem

This paper studies vehicle routing problems on asymmetric metrics. Our starting point is the directed k-TSP problem: given an asymmetric metric (V,d), a root r∈V and a target k≤|V|, compute the minimum length tour that contains r and at least k other vertices. We present a polynomial time O(\fraclog² nloglogn·logk)O(\frac{\log^{2} n}{\log\log n}\cdot\log k)-approximation algorithm for this problem. We use this algorithm for directed k-TSP to obtain an O(\fraclog² nloglogn)O(\frac{\log^{2} n}{\log\log n})-approximation algorithm for the directed orienteering problem. This answers positively, the question of poly-logarithmic approximability of directed orienteering, an open problem from Blum et al. (SIAM J. Comput. 37(2):653–670, 2007). The previously best known results were quasi-polynomial time algorithms with approximation guarantees of O(log ² k) for directed k-TSP, and O(log n) for directed orienteering (Chekuri and Pal in IEEE Symposium on Foundations in Computer Science, pp. 245–253, 2005). Using the algorithm for directed orienteering within the framework of Blum et al. (SIAM J. Comput. 37(2):653–670, 2007) and Bansal et al. (ACM Symposium on Theory of Computing, pp. 166–174, 2004), we also obtain poly-logarithmic approximation algorithms for the directed versions of discounted-reward TSP and vehicle routing problem with time-windows.     

Capabilities and Limits of Compact Error Resilience Methods for Algorithmic Self-Assembly

Winfree’s pioneering work led the foundations in the area of error-reduction in algorithmic self-assembly (Winfree and Bekbolatov in DNA Based Computers 9, LNCS, vol. 2943, pp. 126–144, [2004]), but the construction resulted in increase of the size of assembly. Reif et al. (Nanotechnol. Sci. Comput. 79–103, [2006]) contributed further in this area with compact error-resilient schemes that maintained the original size of the assemblies, but required certain restrictions on the Boolean functions to be used in the algorithmic self-assembly. It is a critical challenge to improve these compact error resilient schemes to incorporate arbitrary Boolean functions, and to determine how far these prior results can be extended under different degrees of restrictions on the Boolean functions. In this work we present a considerably more complete theory of compact error-resilient schemes for algorithmic self-assembly in two and three dimensions. In our error model, ε is defined to be the probability that there is a mismatch between the neighboring sides of two juxtaposed tiles and they still stay together in the equilibrium. This probability is independent of any other match or mismatch and hence we term this probabilistic model as the independent error model. In our model all the error analysis is performed under the assumption of kinetic equilibrium. First we consider two-dimensional algorithmic self-assembly. We present an error correction scheme for reduction of errors from ε to ε ² for arbitrary Boolean functions in two dimensional algorithmic self-assembly. Then we characterize the class of Boolean functions for which the error can be reduced from ε to ε ³, and present an error correction scheme that achieves this reduction. Then we prove ultimate limits on certain classes of compact error resilient schemes: in particular we show that they can not provide reduction of errors from ε to ε ⁴ is for any Boolean functions. Further, we develop the first provable compact error resilience schemes for three dimensional tiling self-assemblies. We also extend the work of Winfree on self-healing in two-dimensional self-assembly (Winfree in Nanotechnol. Sci. Comput. 55–78, [2006]) to obtain a self-healing tile set for three-dimensional self-assembly.     

Ontology-driven coordination model for multiagent-based mobile workforce brokering systems

Coordination has been recognized by many researchers as the most important feature of multi-agent systems. Coordination is defined as managing interdependencies amongst activities (Malone and Crowston in ACM Comput. Surv. 26(1):87–119, 1994). The traditional approach of implementing a coordination mechanism is to hard-wire it into a coordination system at design time. However, in dynamic and open environments, many attributes of the system cannot be accurately identified at the design time. Therefore, dynamic coordination, capable of coordinating activities at run-time, has emerged. On the other hand, a successful dynamic coordination model for multi-agent systems requires knowledge sharing as well as common vocabulary. Therefore, an ontological approach is an appropriate way in proposing dynamic coordination models for multi-agent systems. In this paper, an Ontology-Driven Dynamic Coordination Model (O-DC) for Multiagent-Based Mobile Workforce Brokering Systems (MWBS) (Mousavi et al. in Int. J. Comput. Sci. 6:(5):557–565, 2010; Mousavi et al. in Proceedings of 4th IEEE international symposium on information technology, ITSim’10, Kuala Lumpur, Malaysia, 15–17 June 2010, vol. 3, pp. 1416–1421, 2010; Mousavi and Nordin in Proceedings of the IEEE international conference on electrical engineering and informatics, Bandung, Indonesia, 17–19 June 2007, pp. 294–297, 2007) is proposed and formulated. Subsequently, the applicability of O-DC is examined via simulation based on a real-world scenario.     

Walrasian Equilibrium: Hardness,Approximations and Tractable Instances

We study the complexity issues for Walrasian equilibrium in a special case of combinatorial auction, called single-minded auction, in which every participant is interested in only one subset of commodities. Chen et al. (J. Comput. Syst. Sci. 69(4): 675–687, 2004) showed that it is NP-hard to decide the existence of a Walrasian equilibrium for a single-minded auction and proposed a notion of approximate Walrasian equilibrium called relaxed Walrasian equilibrium. We show that every single-minded auction has a relaxed Walrasian equilibrium that satisfies at least two-thirds of the participants, proving a conjecture posed in Chen et al. (J. Comput. Syst. Sci. 69(4): 675–687, 2004). Motivated by practical considerations, we introduce another concept of approximate Walrasian equilibrium called weak Walrasian equilibrium. We show NP-completeness and hardness of approximation results for weak Walrasian equilibria. In search of positive results, we restrict our attention to the tollbooth problem (Guruswami et al. in Proceedings of the Symposium on Discrete Algorithms (SODA), pp. 1164–1173, 2005), where every participant is interested in a single path in some underlying graph. We give a polynomial time algorithm to determine the existence of a Walrasian equilibrium and compute one (if it exists), when the graph is a tree. However, the problem is still NP-hard for general graphs.     

Network invariants for real-time systems

We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition structures (which are similar in spirit to timed automata) and define a notion of abstraction that is safe with respect to linear temporal properties. We strengthen the notion of abstraction to allow a finite system, then called network invariant, to be an abstraction of networks of real-time systems. In general the problem of checking abstraction of real-time systems is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that one system is an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer’s protocol, using the model checker TLV. Part of this work was done during O. Grinchtein’s stay at Weizmann Institute. This author was supported by the European Research Training Network “Games”.