קולוקוויום וסמינרים

Simon's Factorization Theorem is a powerful tool in the study of formal languages, and is key to many algorithms and theoretical results.

The theorem states that, given a regular language, we can decompose any word to a bounded-height tree that allows reasoning about all infixes of the word in a compact manner. 

In this work, we generalize Simon's factorization theorem to languages of trees. This generalization brings about many challenges involving the manipulation of trees and forests. Specifically, even defining what a decomposition of trees means is highly nontrivial. We provide such a notion, and show how to obtain it (with a caveat).

Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. Most algorithms for deciding if a given system satisfy a given hyperproperty rely on a user-specified abstraction of the system. In this work, we suggest a novel automatic abstraction-refinement algorithm for hyperproperties verification. Our approach is based on predicate abstraction and the recently introduced reduction of hyperproperties verification to satisfiability of Constrained Horn Clauses (CHCs).

Moreover, it formalizes and uses CHC-based refinement for counterexamples in the shape of a directed acyclic graph. We implemented our new algorithm on top of the SMT solver Z3. Our experimental evaluation shows our automatic abstraction refinement algorithm can solve a variety of hyperproperty verification problems, completely automatically. This is in contrast to other existing techniques that require a user-given abstraction.

Real-world reinforcement learning must optimize multiple objectives, satisfy safety constraints, and remain robust to model uncertainty, yet existing methods tackle these challenges in isolation. We introduce Multi-Perspective Actor–Critic (MPAC), a unified framework that combines value decomposition with component-specific risk assessment, enabling safety-critical objectives to act conservatively while performance-oriented objectives retain appropriate optimism.

An influence-based weighting mechanism dynamically adjusts objective importance based on decision relevance and learning progress, eliminating the need for fixed scalarization or prior reward tuning. This produces policies that are simultaneously safe, robust to perturbations, and less conservative than traditional safe or robust RL approaches.

Evaluation on a complex energy-management domain, together with continuous-control benchmarks featuring safety constraints and perturbed dynamics, shows that MPAC consistently achieves stronger multi-objective trade-offs. 

We consider a variant of reachability in Vector Addition Systems (VAS) dubbed box reachability, whereby a vector v in N^d is box-reachable from 0 in a VAS V if V admits a path from 0 to v that not only stays in the positive orthant (as in the standard VAS semantics), but also stays below v, i.e., within the ׳׳box׳׳ whose opposite corners are 0 and v.

Our main result is that for two-dimensional VAS, the set of box-reachable vertices almost coincides with the standard reachability set: the two sets coincide for all vectors whose coordinates are both above some threshold W. We also study properties of box-reachability, exploring the differences and similarities with standard reachability.

Technically, our main result is proved using powerful machinery from convex geometry.

I will present an overview of some topics in computational (and combinatorial, and a bit algebraic) geometry, that constitute milestones in the work in this area by myself and by many colleagues and (former) students in the past 45 years. The topics include, as time permits, algorithmic motion planning, arrangements, lower envelopes, incidences, space decomposition, polynomial partitioning, and more. 

Bio: Micha Sharir received his Ph.D. in Mathematics from Tel Aviv University in 1976, and then switched to Computer Science, doing his postdoctoral studies at the Courant Institute of New York University. He returned to Tel Aviv University in 1980, and has been there, at the School of Computer Science, ever since. He is also a visiting research professor at the Courant Institute, where he has been the deputy head of the Robotics Lab (1985-89). He has served as the head of the Computer Science Department (twice) and as the head of the School of Mathematics (1997-99). He is one of the co-founders of the Minerva Center for Geometry at Tel Aviv University. 

His research interests are in computational and combinatorial geometry and their applications. He has pioneered (with Jack Schwartz) the study of algorithmic motion planning in robotics during the early 1980s, and has been involved in many fundamental research studies that have helped to shape the fields of computational and combinatorial geometry. Among his major achievements, in addition to his earlier work on robotics, are the study of Davenport-Schinzel sequences and their numerous geometric applications, the study of geometric arrangements and their applications, efficient algorithms in geometric optimization (including the introduction and analysis of generalized linear programming), and the study of combinatorial problems involving point configurations, including, since 2008, the application of algebraic techniques to problems involving incidences, distinct and repeated distances, and other related problems in combinatorial and computational geometry. 

His work won him several prizes, including a Max-Planck research prize (1992, jointly with Emo Welzl), the Feher Prize (1999), the Mif'al Hapais' Landau Prize (2002), and the EMET Prize (2007). He is the incumbent of the Nizri Chair in computational geometry and robotics, a Fellow of the Association for Computing Machinery (since 1997), has an honorary doctorate degree from the University of Utrecht (1996), and is a member of the Israeli Academy of Sciences and Humanities (2018). He has supervised 27 Ph.D. students, many of which are now at various stages of an academic career, in Israel and abroad. 

Technion host: Sarah Keren

We introduce a vision-guided robotic system for automated saffron flower harvesting. Using camera-based perception and robotic manipulation, the system detects and cuts whole flowers while preserving their stigmas and avoiding plant damage.