Ashutosh Trivedi | Computer Science | University of Colorado Boulder

Description

Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems. Successful reachability analysis methods for hybrid systems require the unification of techniques from at least two research areas:

Symbolic methods that operate on exact and discrete representations of systems, in the form of various model checking and theorem proving algorithms.
Numerical methods that operate on various forms of numerical approximations and continuous transformations of the systems, as developed in the area of continuous dynamical systems and control theory.

The existing, successful solutions for reachability analysis for hybrid dynamical systems cleverly integrate symbolic and numerical reasoning to tackle the scalability challenge. For instance, the reachable set computation methods explicitly construct flow-pipes that numerically overapproximate the reachable states over time, while efficient computation of such overapproximations requires symbolic representations such as support functions. Similarly, constraint solving methods symbolically encode reachability properties as logic formulas, while solving such formulas requires numerically-driven decision procedures. The key goal of the Symbolic and Numerical Methods for Reachability Analysis (SNR) workshop is to provide a platform to further explore synergies among these approaches by bringing together the experts in these two domains.

Scope

The SNR workshop aims to catalyze work on the interface of symbolic and numerical methods for the reachability analysis. The scope of the workshop includes, but is not restricted to, the following topics:

Verification of hybrid systems
Symbolic representation of regions in reachability analysis
Techniques for Flow-pipe construction
Abstraction techniques for hybrid systems and numerical programs
Trajectory/Counterexample generation from symbolic paths
Techniques for reliable integration
Decision procedures supporting real numbers
Formal logics to reason about hybrid systems
Symbolic and Numerical Methods for Reinforcement Learning and Planning
Domain specific approaches in Biology, Robotics, and Cyber-Physical Systems

Reinforcement Learning (RL) for Real-Time and Hybrid Systems,
Formal Logics for Continuous-State RL (e.g., formal specifications in RL, shielding for RL),
Decision Procedures for Continuous-State RL (e.g. SAT/SMT approaches to infer reward machines),
Deep Neural networks for Symbolic and Numerical Reasoning for Reachability (e.g., neural certificates),
Supervised Learning for SNR (e.g., using decision-trees in generating human-interpretable policies),
Unsupervised Learning for SNR (e.g., mining formal specifications from behaviors), and
Applications of SNR in safety-critical machine learning.

Invited Speakers

Programme

Slot	Speaker	Talk Details
08:50-09:00	Raissi and Trivedi	Opening Remarks
9:00-10:00	Alvaro Velasquez	Of Neurons and Symbols: A Bird's Eye View of Neuro-Symbolic AI
	Alvaro Velasquez is a program manager in the Innovation Information Office (I2O) of the Defense Advanced Research Projects Agency (DARPA), where he currently leads the Assured Neuro-Symbolic Learning and Reasoning (ANSR) program. Before that, Alvaro oversaw the machine intelligence portfolio of investments for the Information Directorate of the Air Force Research Laboratory (AFRL). Alvaro received his PhD in Computer Science from the University of Central Florida and holds an interdisciplinary research record, including publications in artificial intelligence, combinatorial optimization, networking, cloud computing, and logic and circuit design. Alvaro is a recipient of numerous awards, including the National Science Foundation Graduate Research Fellowship Program (NSF GRFP) award, the University of Central Florida 30 Under 30 award, and best paper and patent awards from AFRL. He serves as Associate Editor of IEEE Transactions on Artificial Intelligence and his research has been funded by the Air Force Office of Scientific Research.	Neuro-Symbolic Artificial Intelligence has experienced a renaissance and gained much traction in recent years as a potential “third wave” of AI to follow the tremendously successful second wave underpinned by statistical deep learning. This seeks the integration of neural learning systems and formal symbolic reasoning for more efficient, robust, and explainable AI. Such an integration holds much promise in areas like reinforcement learning and planning, where tremendous progress has been made in recent years, including great feats like the defeat of the world Go champion and powerful agents for real-time strategy games. However, the tremendous success of autonomous decision-making has highlighted its own shortcomings when it comes to data limitations, robustness, and trust, among other things. This talk presents some of these challenges and opportunities facing the development of neurosymbolic autonomy, how this differs from conventional neurosymbolic AI problems like classification and natural language processing, and potential implications to facilitating the broader adoption of autonomous solutions.
10:00-10:30	Coffee Break
10:30-11:30	Necmiye Ozay	Zonotopic Backward Reachability: Efficient Algorithms and Applications in Synthesis and Falsification
	Bio. Necmiye Ozay received her B.S. degree from Bogazici University, Istanbul in 2004, her M.S. degree from the Pennsylvania State University, University Park in 2006 and her Ph.D. degree from Northeastern University, Boston in 2010, all in electrical engineering. She was a postdoctoral scholar at the California Institute of Technology, Pasadena between 2010 and 2013. She joined the University of Michigan, Ann Arbor in 2013, where she is currently an associate professor of Electrical Engineering and Computer Science. She is also a member of the Michigan Robotics Institute. Dr. Ozay’s research interests include hybrid dynamical systems, control, optimization and formal methods with applications in cyber-physical systems, system identification, verification & validation, autonomy and dynamic data analysis. Her papers received several awards. She has received the 1938E Award and a Henry Russel Award from the University of Michigan for her contributions to teaching and research, and five young investigator awards, including NSF CAREER. She is also a recent recipient of the Antonio Ruberti Young Researcher Prize from the IEEE Control Systems Society for her fundamental contributions to the control and identification of hybrid and cyber-physical systems.	Zonotopes are widely used for over-approximating forward reachable sets of uncertain dynamical systems for verification purposes. However, their use for backward reachability, which is relevant for control synthesis, is somewhat limited. The main challenge here is that the backward reachability analysis is a two-player game and involves Minkowski difference operations, but zonotopes are not closed under such operations. In this talk, I will discuss our recent results for inner-approximating backward reachable sets using zonotopes and constrained zonotopes. After a brief discussion of complexity and approximation algorithms, I will present two use cases: one in correct-by-construction control synthesis, second in synthesis guided falsification. Several examples from autonomous systems will be presented, including those using perception-based neural network controllers. Joint work with Liren Yang.
11:30-12:00	Nacim Ramdani	Reachability analysis of hybrid systems
	Bio. Nacim Ramdani is Full Professor of Control Systems Engineering with the Université of Orléans and IUT de Bourges, since september 2010. He is affiliated with the research centre Laboratoire PRISME Univ. Orléans - INSA CVL and the joint Graduate School MIPTIS of the Université of Orléans, INSA CVL, and the Université François Rabelais of Tours, France. He is the head of the "Robotics and ICT" (IRAUS) department of PRISME research centre, since Jan. 2018. His current research interests revolve around developing robust numerical methods for the analysis, monitoring, and control of cyber-physical and autonomous systems in presence of uncertainty, and robust state estimation and data fusion with applications to healthcare, autonomous robotics, smart homes and smart grids. He mainly focuses on interval methods and related set computation techniques.	The talk will emphasize the challenges underlying and the solution techniques for reachability analysis of linear and nonlinear hybrid systems. The talk will describe approaches for flow-pipe computation using interval analysis and set computation techniques. It will then review constraint solving techniques for detecting intersections with guard sets and computing discrete transitions. Finally, it will show how to combine both approaches for seamless hybrid reachability computation.
12:00-12:30	Dominik Wojtczak	Reinforcement Learning for Branching Decision Processes
	Bio. Dominik Wojtczak is a Senior Lecturer (Associate Professor) at the University of Liverpool. He did his PhD at University of Edinburgh, followed by postdoctoral positions at CWI Amsterdam and University of Oxford. His research interests are mainly verification of stochastic systems, game theory and reinforcement learning.	We study reinforcement learning for the optimal control of Branching Markov Decision Processes (BMDPs), a natural extension of (multitype) Branching Markov Chains (BMCs). The state of a (discrete-time) BMCs is a collection of entities of various types that, while spawning other entities, generate a payoff. In comparison with BMCs, where the evolution of each entity of the same type follows the same probabilistic pattern, BMDPs allow an external controller to pick from a range of options. This permits us to study the best/worst behaviour of the system. We generalise model-free reinforcement learning techniques to compute an optimal control strategy of an unknown BMDP in the limit. We present results of an implementation that demonstrate the practicality of the approach.
12:30-14:00	Lunch Break
14:00-15:00	Andreas Rauh	Stochastic, Set-Based and Mixed Uncertainty Representations for the Reachability Analysis of Dynamic Systems
	Bio. Andreas Rauh is a Professor with the Department of Computing Science, Carl von Ossietzky Universität Oldenburg, Germany where he is the head of the group Distributed Control of Interconnected Systems. He received his PhD in 2008 from the Faculty of Engineering and Computer Science at the University of Ulm, Germany working on the "Theory and application of interval methods for analysis and design of robust and optimal controllers of dynamic systems".	Reachability analysis for uncertain dynamic systems can be performed either with the help of stochastic or set-valued approaches, generally representing the notions of aleatory and epistemic uncertainty. Stochastic approaches aim at describing the reachable states in terms of suitable probability distributions. Assuming that a dynamic system is described with the help of a stochastic differential equation in the continuous-time case or with the help of a stochastic difference equation in the discrete-time counterpart, the exact solutions are given with the help of the Fokker-Planck equation (a second-order parabolic partial differential equation) and multi-dimensional nonlinear convolution integrals, respectively. These expressions, however, can only be solved explicitly, both in the continuous- and discrete-time case, if specific assumptions are satisfied. The most well-known case for a closed-form solution is the one of linear dynamic systems with Gaussian representations of the system states and additive normally distributed noise. Then, the closed-form solution of the approaches mentioned above leads to the prediction stage of the Kalman-(Bucy) Filter. In practically all other cases, however, approximations are inevitable. These are given by, just to mention a few alternatives, Gaussian mixture approaches, prediction stages of Unscented Kalman Filters, particle filters, or higher-dimensional models making use of Koopman or Carleman embeddings.
15:00-15:30	Vicenç Puig	Reachability Analysis of Linear Discrete-time Uncertain Systems: Methods and Applications
	Bio. Vicenç Puig received the telecommunications engineering degree in 1993 and the PhD degree in Automatic Control, Vision, and Robotics in 1999, both from Universitat Politècnica de Catalunya (UPC). He is Full Professor of the Automatic Control Department and a Researcher at the Institut de Robòtica i Informàtica Industrial, both from the UPC. He is currently the Director of the Automatic Control Department and Head of the Research Group in Advanced Control Systems at UPC. He has developed important scientific contributions in the areas of fault diagnosis and fault tolerant control using interval and linear-parameter-varying models using set-based approaches. He has participated/leaded more than 20 European and national research projects in the last decade. He has also led many private contracts with several companies and has published more than 200 journal articles and more than 450 in international conference/ workshop proceedings. He has supervised over 30 Ph.D. dissertations and over 50 master’s theses/final projects. He is currently the chair of the IFAC Safeprocess TC Committee 6.4 (2020-until now) and was the vice chair (2014–2017). He has been the general chair of the Third IEEE Conference on Control and Fault-Tolerant Systems (Systol 2016 and 2021) and the IPC chair of the IFAC Safeprocess 2018. He is also Associate Editor in several JCR indexes journals.	In this presentation, the problem of reachability analysis of linear discrete-time uncertain systems will be revised presenting the main problems that appear during the numerical calculations and how the different state-of-art methods try to avoid them. The interest of rechabibility analysis for the considered familiy of systems is presented using several application examples.
15:30-16:00	Coffee Break
16:00-17:00	B Srivathsan	Symbolic enumeration for reachability in timed automata
	B Srivathsan is an Associate Professor at Chennai Mathematical Institute, India. His primary research interest is in the algorithmic analysis of timed automata. His contributions have resulted in the development of T-Checker, an open-source model-checker for timed automata. Apart from this, Srivathsan has worked on subjects revolving around logic, automata and games. Srivathsan completed his PhD at the University of Bordeaux, France and his Masters and Bachelors at the Indian Institute of Technology Bombay, India.	Timed automata are a well established model for the verification of real-time systems, and have been implemented in industry-strength tools. The most successful algorithms for solving reachability in timed automata proceed by systematically enumerating symbolically represented configurations of the automaton. Over the years, several non-trivial techniques have been developed to help terminate this symbolic enumeration as early as possible. In this talk, we will shed light on two central techniques: the first one studies simulations between symbolic states and allows to prune “smaller” states; the second one goes into a local-time semantics for networks of timed automata and manages to tackle the explosion due to concurrency.
17:00-17:30	Akshay S.	Reachability for Pushdown Timed Automta
	Bio. S. Akshay is an associate professor in the Department of Computer Science and Engineering at IIT Bombay. His research interests span formal methods and AI with a focus on automata theory, quantitative (timed/probabilistic) verification and automated functional synthesis. He completed his PhD in 2010 from ENS Cachan (now Univ Paris Saclay), France and Chennai Mathematical Institute, India.	Timed automata and pushdown automata are classical models: the former capture time and the latter recursion. When we mix the two, we get a powerful model of pushdown timed automata (PDTA) that extend classical timed automata with a pushdown LIFO-stack. For timed automata (i.e., without the stack), successful practical algorithms for reachability work by enumerating symbolically represented configurations of the automaton. Surprisingly, for PDTA, despite many theoretical results over the last 25+ years, such algorithms were missing. In this talk, we address this problem by explaining the difficulty posed by the presence of a LIFO-stack. We then develop a modified simulation-based algorithm for PDTA, that handles the stack and is still able to exploit the latest advances in symbolic methods for reachability in timed automata.
17:30-17:40	Raissi and Trivedi	Closing Remarks

Slot

Speaker

Talk Details

08:50-09:00

Raissi and Trivedi

Opening Remarks

9:00-10:00

Alvaro Velasquez

Of Neurons and Symbols: A Bird's Eye View of Neuro-Symbolic AI

Alvaro Velasquez is a program manager in the Innovation Information Office (I2O) of the Defense Advanced Research Projects Agency (DARPA), where he currently leads the Assured Neuro-Symbolic Learning and Reasoning (ANSR) program. Before that, Alvaro oversaw the machine intelligence portfolio of investments for the Information Directorate of the Air Force Research Laboratory (AFRL). Alvaro received his PhD in Computer Science from the University of Central Florida and holds an interdisciplinary research record, including publications in artificial intelligence, combinatorial optimization, networking, cloud computing, and logic and circuit design. Alvaro is a recipient of numerous awards, including the National Science Foundation Graduate Research Fellowship Program (NSF GRFP) award, the University of Central Florida 30 Under 30 award, and best paper and patent awards from AFRL. He serves as Associate Editor of IEEE Transactions on Artificial Intelligence and his research has been funded by the Air Force Office of Scientific Research.

Neuro-Symbolic Artificial Intelligence has experienced a renaissance and gained much traction in recent years as a potential “third wave” of AI to follow the tremendously successful second wave underpinned by statistical deep learning. This seeks the integration of neural learning systems and formal symbolic reasoning for more efficient, robust, and explainable AI. Such an integration holds much promise in areas like reinforcement learning and planning, where tremendous progress has been made in recent years, including great feats like the defeat of the world Go champion and powerful agents for real-time strategy games. However, the tremendous success of autonomous decision-making has highlighted its own shortcomings when it comes to data limitations, robustness, and trust, among other things. This talk presents some of these challenges and opportunities facing the development of neurosymbolic autonomy, how this differs from conventional neurosymbolic AI problems like classification and natural language processing, and potential implications to facilitating the broader adoption of autonomous solutions.

10:00-10:30

Coffee Break

10:30-11:30

Necmiye Ozay

Zonotopic Backward Reachability: Efficient Algorithms and Applications in Synthesis and Falsification

Bio. Necmiye Ozay received her B.S. degree from Bogazici University, Istanbul in 2004, her M.S. degree from the Pennsylvania State University, University Park in 2006 and her Ph.D. degree from Northeastern University, Boston in 2010, all in electrical engineering. She was a postdoctoral scholar at the California Institute of Technology, Pasadena between 2010 and 2013. She joined the University of Michigan, Ann Arbor in 2013, where she is currently an associate professor of Electrical Engineering and Computer Science. She is also a member of the Michigan Robotics Institute. Dr. Ozay’s research interests include hybrid dynamical systems, control, optimization and formal methods with applications in cyber-physical systems, system identification, verification & validation, autonomy and dynamic data analysis. Her papers received several awards. She has received the 1938E Award and a Henry Russel Award from the University of Michigan for her contributions to teaching and research, and five young investigator awards, including NSF CAREER. She is also a recent recipient of the Antonio Ruberti Young Researcher Prize from the IEEE Control Systems Society for her fundamental contributions to the control and identification of hybrid and cyber-physical systems.

Zonotopes are widely used for over-approximating forward reachable sets of uncertain dynamical systems for verification purposes. However, their use for backward reachability, which is relevant for control synthesis, is somewhat limited. The main challenge here is that the backward reachability analysis is a two-player game and involves Minkowski difference operations, but zonotopes are not closed under such operations. In this talk, I will discuss our recent results for inner-approximating backward reachable sets using zonotopes and constrained zonotopes. After a brief discussion of complexity and approximation algorithms, I will present two use cases: one in correct-by-construction control synthesis, second in synthesis guided falsification. Several examples from autonomous systems will be presented, including those using perception-based neural network controllers. Joint work with Liren Yang.

11:30-12:00

Nacim Ramdani

Reachability analysis of hybrid systems

Bio. Nacim Ramdani is Full Professor of Control Systems Engineering with the Université of Orléans and IUT de Bourges, since september 2010. He is affiliated with the research centre Laboratoire PRISME Univ. Orléans - INSA CVL and the joint Graduate School MIPTIS of the Université of Orléans, INSA CVL, and the Université François Rabelais of Tours, France. He is the head of the "Robotics and ICT" (IRAUS) department of PRISME research centre, since Jan. 2018. His current research interests revolve around developing robust numerical methods for the analysis, monitoring, and control of cyber-physical and autonomous systems in presence of uncertainty, and robust state estimation and data fusion with applications to healthcare, autonomous robotics, smart homes and smart grids. He mainly focuses on interval methods and related set computation techniques.

The talk will emphasize the challenges underlying and the solution techniques for reachability analysis of linear and nonlinear hybrid systems. The talk will describe approaches for flow-pipe computation using interval analysis and set computation techniques. It will then review constraint solving techniques for detecting intersections with guard sets and computing discrete transitions. Finally, it will show how to combine both approaches for seamless hybrid reachability computation.

12:00-12:30

Dominik Wojtczak

Reinforcement Learning for Branching Decision Processes

Bio. Dominik Wojtczak is a Senior Lecturer (Associate Professor) at the University of Liverpool. He did his PhD at University of Edinburgh, followed by postdoctoral positions at CWI Amsterdam and University of Oxford. His research interests are mainly verification of stochastic systems, game theory and reinforcement learning.

We study reinforcement learning for the optimal control of Branching Markov Decision Processes (BMDPs), a natural extension of (multitype) Branching Markov Chains (BMCs). The state of a (discrete-time) BMCs is a collection of entities of various types that, while spawning other entities, generate a payoff. In comparison with BMCs, where the evolution of each entity of the same type follows the same probabilistic pattern, BMDPs allow an external controller to pick from a range of options. This permits us to study the best/worst behaviour of the system. We generalise model-free reinforcement learning techniques to compute an optimal control strategy of an unknown BMDP in the limit. We present results of an implementation that demonstrate the practicality of the approach.

12:30-14:00

Lunch Break

14:00-15:00

Andreas Rauh

Stochastic, Set-Based and Mixed Uncertainty Representations for the Reachability Analysis of Dynamic Systems

Bio. Andreas Rauh is a Professor with the Department of Computing Science, Carl von Ossietzky Universität Oldenburg, Germany where he is the head of the group Distributed Control of Interconnected Systems. He received his PhD in 2008 from the Faculty of Engineering and Computer Science at the University of Ulm, Germany working on the "Theory and application of interval methods for analysis and design of robust and optimal controllers of dynamic systems".

Reachability analysis for uncertain dynamic systems can be performed either with the help of stochastic or set-valued approaches, generally representing the notions of aleatory and epistemic uncertainty. Stochastic approaches aim at describing the reachable states in terms of suitable probability distributions. Assuming that a dynamic system is described with the help of a stochastic differential equation in the continuous-time case or with the help of a stochastic difference equation in the discrete-time counterpart, the exact solutions are given with the help of the Fokker-Planck equation (a second-order parabolic partial differential equation) and multi-dimensional nonlinear convolution integrals, respectively. These expressions, however, can only be solved explicitly, both in the continuous- and discrete-time case, if specific assumptions are satisfied. The most well-known case for a closed-form solution is the one of linear dynamic systems with Gaussian representations of the system states and additive normally distributed noise. Then, the closed-form solution of the approaches mentioned above leads to the prediction stage of the Kalman-(Bucy) Filter. In practically all other cases, however, approximations are inevitable. These are given by, just to mention a few alternatives, Gaussian mixture approaches, prediction stages of Unscented Kalman Filters, particle filters, or higher-dimensional models making use of Koopman or Carleman embeddings.

15:00-15:30

Vicenç Puig

Reachability Analysis of Linear Discrete-time Uncertain Systems: Methods and Applications

Bio. Vicenç Puig received the telecommunications engineering degree in 1993 and the PhD degree in Automatic Control, Vision, and Robotics in 1999, both from Universitat Politècnica de Catalunya (UPC). He is Full Professor of the Automatic Control Department and a Researcher at the Institut de Robòtica i Informàtica Industrial, both from the UPC. He is currently the Director of the Automatic Control Department and Head of the Research Group in Advanced Control Systems at UPC. He has developed important scientific contributions in the areas of fault diagnosis and fault tolerant control using interval and linear-parameter-varying models using set-based approaches. He has participated/leaded more than 20 European and national research projects in the last decade. He has also led many private contracts with several companies and has published more than 200 journal articles and more than 450 in international conference/ workshop proceedings. He has supervised over 30 Ph.D. dissertations and over 50 master’s theses/final projects. He is currently the chair of the IFAC Safeprocess TC Committee 6.4 (2020-until now) and was the vice chair (2014–2017). He has been the general chair of the Third IEEE Conference on Control and Fault-Tolerant Systems (Systol 2016 and 2021) and the IPC chair of the IFAC Safeprocess 2018. He is also Associate Editor in several JCR indexes journals.

In this presentation, the problem of reachability analysis of linear discrete-time uncertain systems will be revised presenting the main problems that appear during the numerical calculations and how the different state-of-art methods try to avoid them. The interest of rechabibility analysis for the considered familiy of systems is presented using several application examples.

15:30-16:00

Coffee Break

16:00-17:00

B Srivathsan

Symbolic enumeration for reachability in timed automata

B Srivathsan is an Associate Professor at Chennai Mathematical Institute, India. His primary research interest is in the algorithmic analysis of timed automata. His contributions have resulted in the development of T-Checker, an open-source model-checker for timed automata. Apart from this, Srivathsan has worked on subjects revolving around logic, automata and games. Srivathsan completed his PhD at the University of Bordeaux, France and his Masters and Bachelors at the Indian Institute of Technology Bombay, India.

Timed automata are a well established model for the verification of real-time systems, and have been implemented in industry-strength tools. The most successful algorithms for solving reachability in timed automata proceed by systematically enumerating symbolically represented configurations of the automaton. Over the years, several non-trivial techniques have been developed to help terminate this symbolic enumeration as early as possible. In this talk, we will shed light on two central techniques: the first one studies simulations between symbolic states and allows to prune “smaller” states; the second one goes into a local-time semantics for networks of timed automata and manages to tackle the explosion due to concurrency.

17:00-17:30

Akshay S.

Reachability for Pushdown Timed Automta

Bio. S. Akshay is an associate professor in the Department of Computer Science and Engineering at IIT Bombay. His research interests span formal methods and AI with a focus on automata theory, quantitative (timed/probabilistic) verification and automated functional synthesis. He completed his PhD in 2010 from ENS Cachan (now Univ Paris Saclay), France and Chennai Mathematical Institute, India.

Timed automata and pushdown automata are classical models: the former capture time and the latter recursion. When we mix the two, we get a powerful model of pushdown timed automata (PDTA) that extend classical timed automata with a pushdown LIFO-stack. For timed automata (i.e., without the stack), successful practical algorithms for reachability work by enumerating symbolically represented configurations of the automaton. Surprisingly, for PDTA, despite many theoretical results over the last 25+ years, such algorithms were missing. In this talk, we address this problem by explaining the difficulty posed by the presence of a LIFO-stack. We then develop a modified simulation-based algorithm for PDTA, that handles the stack and is still able to exploit the latest advances in symbolic methods for reachability in timed automata.

17:30-17:40

Raissi and Trivedi

Closing Remarks

Organizers

Submission Information

The workshop solicits

long research papers (not exceeding 15 pages excluding references),
short research papers (not exceeding 6 pages excluding references) and
work-in-progress papers (not exceeding 6 pages excluding references).

Research papers must present original unpublished work which is not submitted elsewhere. In order to foster the exchange of ideas, we also encourage work-in-progress papers, which present recent or on-going work. The papers should be written in English and formatted according to the EPTCS guidelines. Papers can be submitted using the EasyChair system. All submissions will undergo a peer-reviewing process.

Accepted research papers will be presented at the workshop and will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Accepted work-in-progress papers will be presented at the workshop but will not be included in the proceedings.