SPaC: a symbolic pareto calculator

ABSTRACT

The compositional computation of Pareto points in multi-dimensional optimization problems is an important means to efficiently explore the optimization space. This paper presents a symbolic Pareto calculator, SPaC, for the algebraic computation of multidimensional trade-offs. SPaC uses BDDs as a representation for solution sets and operations on them. The tool can be used in multi-criteria optimization and design-space exploration of embedded systems. The paper describes the design and implementation of Pareto algebra operations, and it shows that BDDs can be used effectively in Pareto optimization.

REFERENCES

• 1: Parosh Aziz Abdulla , Bengt Jonsson , Marcus Nilsson , Julien d'Orso, Regular Model Checking Made Simple and Efficient, Proceedings of the 13th International Conference on Concurrency Theory, p.116-130, August 20-23, 2002
• 2: Md. Mostofa Akbar , M. Sohel Rahman , M. Kaykobad , E. G. Manning , G. C. Shoja, Solving the multidimensional multiple-choice knapsack problem by constructing convex hulls, Computers and Operations Research, v.33 n.5, p.1259-1273, May 2006 [doi>10.1016/j.cor.2004.09.016]
• 3: Rudolf Berghammer , Barbara Leoniuk , Ulf Milanese, Implementation of Relational Algebra Using Binary Decision Diagrams, Revised Papers from the 6th International Conference and 1st Workshop of COST Action 274 TARSKI on Relational Methods in Computer Science, p.241-257, October 16-21, 2001
• 4: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 5: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 6: Maciej Ciesielski , Priyank Kalla , Serkan Askar, Taylor Expansion Diagrams: A Canonical Representation for Verification of Data Flow Designs, IEEE Transactions on Computers, v.55 n.9, p.1188-1201, September 2006 [doi>10.1109/TC.2006.153]
• 7: Marc Geilen , Twan Basten, A calculator for Pareto points, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 8: Marc Geilen , Twan Basten , Bart Theelen , Ralph Otten, An Algebra of Pareto Points, Fundamenta Informaticae, v.78 n.1, p.35-74, September 2007
• 9: Jesper G. Henriksen , Jakob L. Jensen , Michael E. Jørgensen , Nils Klarlund , Robert Paige , Theis Rauhe , Anders Sandholm, Mona: Monadic Second-Order Logic in Practice, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.89-110, May 19-20, 1995
• 10: Rob Hoes , Twan Basten , Chen-Khong Tham , Marc Geilen , Henk Corporaal, Analysing qos trade-offs in wireless sensor networks, Proceedings of the 10th ACM Symposium on Modeling, analysis, and simulation of wireless and mobile systems, October 22-26, 2007, Chania, Crete Island, Greece [doi>10.1145/1298126.1298140]
• 11: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 12: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, ACM SIGPLAN Notices, v.39 n.6, May 2004
• 13: F. Somenzi. Cudd: Cu decision diagram package, http://vlsi.colorado.edu/~fabio/cudd.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation
          Subjects: Representations (general and polynomial)

General Terms:
Algorithms, Design, Experimentation

Keywords:
binay decision diagram, embedded systems, pareto algeba