Showing 1–6 of 6 results for author: Maler, O

Learning Regular Languages over Large Ordered Alphabets

Authors: Irini-Eleftheria Mens, Oded Maler

Abstract: This work is concerned with regular languages defined over large alphabets, either infinite or just too large to be expressed enumeratively. We define a generic model where transitions are labeled by elements of a finite partition of the alphabet. We then extend Angluin's L* algorithm for learning regular languages from examples for such automata. We have implemented this algorithm and we demonst… ▽ More This work is concerned with regular languages defined over large alphabets, either infinite or just too large to be expressed enumeratively. We define a generic model where transitions are labeled by elements of a finite partition of the alphabet. We then extend Angluin's L* algorithm for learning regular languages from examples for such automata. We have implemented this algorithm and we demonstrate its behavior where the alphabet is a subset of the natural or real numbers. We sketch the extension of the algorithm to a class of languages over partially ordered alphabets. △ Less

Submitted 16 September, 2015; v1 submitted 1 June, 2015; originally announced June 2015.

Journal ref: Logical Methods in Computer Science, Volume 11, Issue 3 (September 17, 2015) lmcs:1589

Formal and Informal Methods for Multi-Core Design Space Exploration

Authors: Jean-Francois Kempf, Olivier Lebeltel, Oded Maler

Abstract: We propose a tool-supported methodology for design-space exploration for embedded systems. It provides means to define high-level models of applications and multi-processor architectures and evaluate the performance of different deployment (mapping, scheduling) strategies while taking uncertainty into account. We argue that this extension of the scope of formal verification is important for the vi… ▽ More We propose a tool-supported methodology for design-space exploration for embedded systems. It provides means to define high-level models of applications and multi-processor architectures and evaluate the performance of different deployment (mapping, scheduling) strategies while taking uncertainty into account. We argue that this extension of the scope of formal verification is important for the viability of the domain. △ Less

Submitted 8 June, 2014; originally announced June 2014.

Comments: In Proceedings QAPL 2014, arXiv:1406.1567

Journal ref: EPTCS 154, 2014, pp. 78-92

Algorithmic Verification of Continuous and Hybrid Systems

Authors: Oded Maler

Abstract: We provide a tutorial introduction to reachability computation, a class of computational techniques that exports verification technology toward continuous and hybrid systems. For open under-determined systems, this technique can sometimes replace an infinite number of simulations. We provide a tutorial introduction to reachability computation, a class of computational techniques that exports verification technology toward continuous and hybrid systems. For open under-determined systems, this technique can sometimes replace an infinite number of simulations. △ Less

Submitted 26 February, 2014; originally announced March 2014.

Comments: In Proceedings INFINITY 2013, arXiv:1402.6610

Journal ref: EPTCS 140, 2014, pp. 48-69

Exploring the Dynamics of Mass Action Systems

Authors: Oded Maler, Ádám M. Halász, Olivier Lebeltel, Ouri Maler

Abstract: We present the Populus toolkit for exploring the dynamics of mass action systems under different assumptions. We present the Populus toolkit for exploring the dynamics of mass action systems under different assumptions. △ Less

Submitted 3 September, 2013; originally announced September 2013.

Comments: In Proceedings HSB 2013, arXiv:1308.5724

Journal ref: EPTCS 125, 2013, pp. 84-91

A Framework for Control Strategies in Uncertain Inference Networks

Authors: Moshe Ben-Bassat, Oded Maler

Abstract: Control Strategies for hierarchical tree-like probabilistic inference networks are formulated and investigated. Strategies that utilize staged look-ahead and temporary focus on subgoals are formalized and refined using the Depth Vector concept that serves as a tool for defining the 'virtual tree' regarded by the control strategy. The concept is illustrated by four types of control strategies for t… ▽ More Control Strategies for hierarchical tree-like probabilistic inference networks are formulated and investigated. Strategies that utilize staged look-ahead and temporary focus on subgoals are formalized and refined using the Depth Vector concept that serves as a tool for defining the 'virtual tree' regarded by the control strategy. The concept is illustrated by four types of control strategies for three-level trees that are characterized according to their Depth Vector, and according to the way they consider intermediate nodes and the role that they let these nodes play. INFERENTI is a computerized inference system written in Prolog, which provides tools for exercising a variety of control strategies. The system also provides tools for simulating test data and for comparing the relative average performance under different strategies. △ Less

Submitted 27 March, 2013; originally announced April 2013.

Comments: Appears in Proceedings of the First Conference on Uncertainty in Artificial Intelligence (UAI1985)

Report number: UAI-P-1985-PG-143-151

On Zone-Based Analysis of Duration Probabilistic Automata

Authors: Oded Maler, Kim G. Larsen, Bruce H. Krogh

Abstract: We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as probabilistic rather than set-theoretic. We study duration probabilistic automata (DPA), expressing multiple parallel processes admitting memoryfull continuously-distributed durations. For this model we develop an extension of the zone-based forward reach… ▽ More We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as probabilistic rather than set-theoretic. We study duration probabilistic automata (DPA), expressing multiple parallel processes admitting memoryfull continuously-distributed durations. For this model we develop an extension of the zone-based forward reachability algorithm whose successor operator is a density transformer, thus providing a solution to verification and performance evaluation problems concerning acyclic DPA (or the bounded-horizon behavior of cyclic DPA). △ Less

Submitted 31 October, 2010; originally announced November 2010.

Comments: In Proceedings INFINITY 2010, arXiv:1010.6112

Journal ref: EPTCS 39, 2010, pp. 33-46